/usr/share/matita/lib/basics/deqsets.ma is in matita 0.99.1-3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 | (*
||M|| This file is part of HELM, an Hypertextual, Electronic
||A|| Library of Mathematics, developed at the Computer Science
||T|| Department of the University of Bologna, Italy.
||I||
||T||
||A||
\ / This file is distributed under the terms of the
\ / GNU General Public License Version 2
V_______________________________________________________________ *)
include "basics/types.ma".
include "basics/bool.ma".
(****** DeqSet: a set with a decidbale equality ******)
record DeqSet : Type[1] ≝ { carr :> Type[0];
eqb: carr → carr → bool;
eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)
}.
notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
interpretation "eqb" 'eqb a b = (eqb ? a b).
notation "\P H" non associative with precedence 90
for @{(proj1 … (eqb_true ???) $H)}.
notation "\b H" non associative with precedence 90
for @{(proj2 … (eqb_true ???) $H)}.
lemma eqb_false: ∀S:DeqSet.∀a,b:S.
(eqb ? a b) = false ↔ a ≠ b.
#S #a #b % #H
[@(not_to_not … not_eq_true_false) #H1 <H @sym_eq @(\b H1)
|cases (true_or_false (eqb ? a b)) // #H1 @False_ind @(absurd … (\P H1) H)
]
qed.
notation "\Pf H" non associative with precedence 90
for @{(proj1 … (eqb_false ???) $H)}.
notation "\bf H" non associative with precedence 90
for @{(proj2 … (eqb_false ???) $H)}.
lemma dec_eq: ∀S:DeqSet.∀a,b:S. a = b ∨ a ≠ b.
#S #a #b cases (true_or_false (eqb ? a b)) #H
[%1 @(\P H) | %2 @(\Pf H)]
qed.
definition beqb ≝ λb1,b2.
match b1 with [ true ⇒ b2 | false ⇒ notb b2].
notation < "a == b" non associative with precedence 45 for @{beqb $a $b }.
lemma beqb_true: ∀b1,b2. iff (beqb b1 b2 = true) (b1 = b2).
#b1 #b2 cases b1 cases b2 normalize /2/
qed.
definition DeqBool ≝ mk_DeqSet bool beqb beqb_true.
unification hint 0 ≔ ;
X ≟ mk_DeqSet bool beqb beqb_true
(* ---------------------------------------- *) ⊢
bool ≡ carr X.
unification hint 0 ≔ b1,b2:bool;
X ≟ mk_DeqSet bool beqb beqb_true
(* ---------------------------------------- *) ⊢
beqb b1 b2 ≡ eqb X b1 b2.
example exhint: ∀b:bool. (b == false) = true → b = false.
#b #H @(\P H).
qed.
(* pairs *)
definition eq_pairs ≝
λA,B:DeqSet.λp1,p2:A×B.(\fst p1 == \fst p2) ∧ (\snd p1 == \snd p2).
lemma eq_pairs_true: ∀A,B:DeqSet.∀p1,p2:A×B.
eq_pairs A B p1 p2 = true ↔ p1 = p2.
#A #B * #a1 #b1 * #a2 #b2 %
[#H cases (andb_true …H) #eqa #eqb >(\P eqa) >(\P eqb) //
|#H destruct normalize >(\b (refl … a2)) >(\b (refl … b2)) //
]
qed.
definition DeqProd ≝ λA,B:DeqSet.
mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
unification hint 0 ≔ C1,C2;
T1 ≟ carr C1,
T2 ≟ carr C2,
X ≟ DeqProd C1 C2
(* ---------------------------------------- *) ⊢
T1×T2 ≡ carr X.
unification hint 0 ≔ T1,T2,p1,p2;
X ≟ DeqProd T1 T2
(* ---------------------------------------- *) ⊢
eq_pairs T1 T2 p1 p2 ≡ eqb X p1 p2.
example hint2: ∀b1,b2.
〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.
#b1 #b2 #H @(\P H).
|