example ex1 : \fst (equiv ? (exp8+exp9) exp9) = true.
normalize // qed.
+definition exp10 ≝ a·a·a·a·a·a·a·a·a·a·a·a·(a^* ).
+definition exp11 ≝ (a·a·a·a·a + a·a·a·a·a·a·a)^*.
-
+example ex2 : \fst (equiv ? (exp10+exp11) exp10) = true.
+normalize // qed.
--- /dev/null
+include "basics/relations.ma".
+
+(********** bool **********)
+inductive bool: Type[0] ≝
+ | true : bool
+ | false : bool.
+
+theorem not_eq_true_false : true ≠ false.
+@nmk #Heq destruct
+qed.
+
+definition notb : bool → bool ≝
+λ b:bool. match b with [true ⇒ false|false ⇒ true ].
+
+interpretation "boolean not" 'not x = (notb x).
+
+theorem notb_elim: ∀ b:bool.∀ P:bool → Prop.
+match b with
+[ true ⇒ P false
+| false ⇒ P true] → P (notb b).
+#b #P elim b normalize // qed.
+
+theorem notb_notb: ∀b:bool. notb (notb b) = b.
+#b elim b // qed.
+
+theorem injective_notb: injective bool bool notb.
+#b1 #b2 #H <(notb_notb b1) <(notb_notb b2) @eq_f // qed.
+
+theorem noteq_to_eqnot: ∀b1,b2. b1 ≠ b2 → b1 = notb b2.
+* * // #H @False_ind /2/
+qed.
+
+theorem eqnot_to_noteq: ∀b1,b2. b1 = notb b2 → b1 ≠ b2.
+* * normalize // #H @(not_to_not … not_eq_true_false) //
+qed.
+
+definition andb : bool → bool → bool ≝
+λb1,b2:bool. match b1 with [ true ⇒ b2 | false ⇒ false ].
+
+interpretation "boolean and" 'and x y = (andb x y).
+
+theorem andb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop.
+match b1 with [ true ⇒ P b2 | false ⇒ P false] → P (b1 ∧ b2).
+#b1 #b2 #P (elim b1) normalize // qed.
+
+theorem andb_true_l: ∀ b1,b2. (b1 ∧ b2) = true → b1 = true.
+#b1 (cases b1) normalize // qed.
+
+theorem andb_true_r: ∀b1,b2. (b1 ∧ b2) = true → b2 = true.
+#b1 #b2 (cases b1) normalize // (cases b2) // qed.
+
+theorem andb_true: ∀b1,b2. (b1 ∧ b2) = true → b1 = true ∧ b2 = true.
+/3/ qed.
+
+definition orb : bool → bool → bool ≝
+λb1,b2:bool.match b1 with [ true ⇒ true | false ⇒ b2].
+
+interpretation "boolean or" 'or x y = (orb x y).
+
+theorem orb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop.
+match b1 with [ true ⇒ P true | false ⇒ P b2] → P (orb b1 b2).
+#b1 #b2 #P (elim b1) normalize // qed.
+
+lemma orb_true_r1: ∀b1,b2:bool.
+ b1 = true → (b1 ∨ b2) = true.
+#b1 #b2 #H >H // qed.
+
+lemma orb_true_r2: ∀b1,b2:bool.
+ b2 = true → (b1 ∨ b2) = true.
+#b1 #b2 #H >H cases b1 // qed.
+
+lemma orb_true_l: ∀b1,b2:bool.
+ (b1 ∨ b2) = true → (b1 = true) ∨ (b2 = true).
+* normalize /2/ qed.
+
+definition xorb : bool → bool → bool ≝
+λb1,b2:bool.
+ match b1 with
+ [ true ⇒ match b2 with [ true ⇒ false | false ⇒ true ]
+ | false ⇒ match b2 with [ true ⇒ true | false ⇒ false ]].
+
+notation > "'if' term 46 e 'then' term 46 t 'else' term 46 f" non associative with precedence 46
+ for @{ match $e in bool with [ true ⇒ $t | false ⇒ $f] }.
+notation < "hvbox('if' \nbsp term 46 e \nbsp break 'then' \nbsp term 46 t \nbsp break 'else' \nbsp term 49 f \nbsp)" non associative with precedence 46
+ for @{ match $e with [ true ⇒ $t | false ⇒ $f] }.
+
+theorem bool_to_decidable_eq:
+ ∀b1,b2:bool. decidable (b1=b2).
+#b1 #b2 (cases b1) (cases b2) /2/ %2 /3/ qed.
+
+theorem true_or_false:
+∀b:bool. b = true ∨ b = false.
+#b (cases b) /2/ qed.
+
+
--- /dev/null
+(* exists *******************************************************************)
+
+notation "hvbox(∃ _ break . p)"
+ with precedence 20
+for @{'exists $p }.
+
+notation < "hvbox(\exists ident i : ty break . p)"
+ right associative with precedence 20
+for @{'exists (\lambda ${ident i} : $ty. $p) }.
+
+notation < "hvbox(\exists ident i break . p)"
+ with precedence 20
+for @{'exists (\lambda ${ident i}. $p) }.
+
+(*
+notation < "hvbox(\exists ident i opt (: ty) break . p)"
+ right associative with precedence 20
+for @{ 'exists ${default
+ @{\lambda ${ident i} : $ty. $p}
+ @{\lambda ${ident i} . $p}}}.
+*)
+
+notation > "\exists list1 ident x sep , opt (: T). term 19 Px"
+ with precedence 20
+ for ${ default
+ @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}:$T.$acc)} } }
+ @{ ${ fold right @{$Px} rec acc @{'exists (λ${ident x}.$acc)} } }
+ }.
+
+(* sigma ********************************************************************)
+
+notation < "hvbox(\Sigma ident i : ty break . p)"
+ left associative with precedence 20
+for @{'sigma (\lambda ${ident i} : $ty. $p) }.
+
+notation < "hvbox(\Sigma ident i break . p)"
+ with precedence 20
+for @{'sigma (\lambda ${ident i}. $p) }.
+
+(*
+notation < "hvbox(\Sigma ident i opt (: ty) break . p)"
+ right associative with precedence 20
+for @{ 'sigma ${default
+ @{\lambda ${ident i} : $ty. $p}
+ @{\lambda ${ident i} . $p}}}.
+*)
+
+notation > "\Sigma list1 ident x sep , opt (: T). term 19 Px"
+ with precedence 20
+ for ${ default
+ @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}:$T.$acc)} } }
+ @{ ${ fold right @{$Px} rec acc @{'sigma (λ${ident x}.$acc)} } }
+ }.
+
+notation "hvbox(« term 19 a, break term 19 b»)"
+with precedence 90 for @{ 'dp $a $b }.
+
+(* dependent pairs (i.e. Sigma with predicate in Type[0]) ********************)
+
+notation < "hvbox(𝚺 ident i : ty break . p)"
+ left associative with precedence 20
+for @{'dpair (\lambda ${ident i} : $ty. $p) }.
+
+notation < "hvbox(𝚺 ident i break . p)"
+ with precedence 20
+for @{'dpair (\lambda ${ident i}. $p) }.
+
+(*
+notation < "hvbox(𝚺 ident i opt (: ty) break . p)"
+ right associative with precedence 20
+for @{ 'dpair ${default
+ @{\lambda ${ident i} : $ty. $p}
+ @{\lambda ${ident i} . $p}}}.
+*)
+
+notation > "𝚺 list1 ident x sep , opt (: T). term 19 Px"
+ with precedence 20
+ for ${ default
+ @{ ${ fold right @{$Px} rec acc @{'dpair (λ${ident x}:$T.$acc)} } }
+ @{ ${ fold right @{$Px} rec acc @{'dpair (λ${ident x}.$acc)} } }
+ }.
+
+notation "hvbox(❬ term 19 a, break term 19 b❭)"
+with precedence 90 for @{ 'mk_DPair $a $b }.
+
+(* equality, conguence ******************************************************)
+
+notation > "hvbox(a break = b)"
+ non associative with precedence 45
+for @{ 'eq ? $a $b }.
+
+notation < "hvbox(term 46 a break maction (=) (=\sub t) term 46 b)"
+ non associative with precedence 45
+for @{ 'eq $t $a $b }.
+
+notation > "hvbox(n break (≅ \sub term 90 p) m)"
+ non associative with precedence 45
+for @{ 'congruent $n $m $p }.
+
+notation < "hvbox(term 46 n break ≅ \sub p term 46 m)"
+ non associative with precedence 45
+for @{ 'congruent $n $m $p }.
+
+(* other notations **********************************************************)
+
+notation "hvbox(\langle term 19 a, break term 19 b\rangle)"
+with precedence 90 for @{ 'pair $a $b}.
+
+notation "hvbox(x break \times y)" with precedence 70
+for @{ 'product $x $y}.
+
+notation < "\fst \nbsp term 90 x" with precedence 69 for @{'pi1a $x}.
+notation < "\snd \nbsp term 90 x" with precedence 69 for @{'pi2a $x}.
+
+notation < "\fst \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi1b $x $y}.
+notation < "\snd \nbsp term 90 x \nbsp term 90 y" with precedence 69 for @{'pi2b $x $y}.
+
+notation > "\fst" with precedence 90 for @{'pi1}.
+notation > "\snd" with precedence 90 for @{'pi2}.
+
+notation "hvbox(a break \to b)"
+ right associative with precedence 20
+for @{ \forall $_:$a.$b }.
+
+notation < "hvbox(a break \to b)"
+ right associative with precedence 20
+for @{ \Pi $_:$a.$b }.
+
+notation "hvbox(a break \leq b)"
+ non associative with precedence 45
+for @{ 'leq $a $b }.
+
+notation "hvbox(a break \geq b)"
+ non associative with precedence 45
+for @{ 'geq $a $b }.
+
+notation "hvbox(a break \lt b)"
+ non associative with precedence 45
+for @{ 'lt $a $b }.
+
+notation "hvbox(a break \gt b)"
+ non associative with precedence 45
+for @{ 'gt $a $b }.
+
+notation > "hvbox(a break \neq b)"
+ non associative with precedence 45
+for @{ 'neq ? $a $b }.
+
+notation < "hvbox(a break maction (\neq) (\neq\sub t) b)"
+ non associative with precedence 45
+for @{ 'neq $t $a $b }.
+
+notation "hvbox(a break \nleq b)"
+ non associative with precedence 45
+for @{ 'nleq $a $b }.
+
+notation "hvbox(a break \ngeq b)"
+ non associative with precedence 45
+for @{ 'ngeq $a $b }.
+
+notation "hvbox(a break \nless b)"
+ non associative with precedence 45
+for @{ 'nless $a $b }.
+
+notation "hvbox(a break \ngtr b)"
+ non associative with precedence 45
+for @{ 'ngtr $a $b }.
+
+notation "hvbox(a break \divides b)"
+ non associative with precedence 45
+for @{ 'divides $a $b }.
+
+notation "hvbox(a break \ndivides b)"
+ non associative with precedence 45
+for @{ 'ndivides $a $b }.
+
+notation "hvbox(a break + b)"
+ left associative with precedence 50
+for @{ 'plus $a $b }.
+
+notation "hvbox(a break - b)"
+ left associative with precedence 50
+for @{ 'minus $a $b }.
+
+notation "hvbox(a break * b)"
+ left associative with precedence 55
+for @{ 'times $a $b }.
+
+notation "hvbox(a break \middot b)"
+ left associative with precedence 55
+ for @{ 'middot $a $b }.
+
+notation "hvbox(a break \mod b)"
+ left associative with precedence 55
+for @{ 'module $a $b }.
+
+notation < "a \frac b"
+ non associative with precedence 90
+for @{ 'divide $a $b }.
+
+notation "a \over b"
+ left associative with precedence 55
+for @{ 'divide $a $b }.
+
+notation "hvbox(a break / b)"
+ left associative with precedence 55
+for @{ 'divide $a $b }.
+
+notation "- term 60 a" with precedence 60
+for @{ 'uminus $a }.
+
+notation "a !"
+ non associative with precedence 80
+for @{ 'fact $a }.
+
+notation "\sqrt a"
+ non associative with precedence 60
+for @{ 'sqrt $a }.
+
+notation "hvbox(a break \lor b)"
+ left associative with precedence 30
+for @{ 'or $a $b }.
+
+notation "hvbox(a break \land b)"
+ left associative with precedence 35
+for @{ 'and $a $b }.
+
+notation "hvbox(\lnot a)"
+ non associative with precedence 40
+for @{ 'not $a }.
+
+notation > "hvbox(a break \liff b)"
+ left associative with precedence 25
+for @{ 'iff $a $b }.
+
+notation "hvbox(a break \leftrightarrow b)"
+ left associative with precedence 25
+for @{ 'iff $a $b }.
+
+
+notation "hvbox(\Omega \sup term 90 A)" non associative with precedence 90
+for @{ 'powerset $A }.
+notation > "hvbox(\Omega ^ term 90 A)" non associative with precedence 90
+for @{ 'powerset $A }.
+
+notation < "hvbox({ ident i | term 19 p })" with precedence 90
+for @{ 'subset (\lambda ${ident i} : $nonexistent . $p)}.
+
+notation > "hvbox({ ident i | term 19 p })" with precedence 90
+for @{ 'subset (\lambda ${ident i}. $p)}.
+
+notation < "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
+for @{ 'comprehension $s (\lambda ${ident i} : $nonexistent . $p)}.
+
+notation > "hvbox({ ident i ∈ s | term 19 p })" with precedence 90
+for @{ 'comprehension $s (\lambda ${ident i}. $p)}.
+
+notation "hvbox(a break ∈ b)" non associative with precedence 45
+for @{ 'mem $a $b }.
+
+notation "hvbox(a break ≬ b)" non associative with precedence 45
+for @{ 'overlaps $a $b }. (* \between *)
+
+notation "hvbox(a break ⊆ b)" non associative with precedence 45
+for @{ 'subseteq $a $b }. (* \subseteq *)
+
+notation "hvbox(a break ∩ b)" left associative with precedence 55
+for @{ 'intersects $a $b }. (* \cap *)
+
+notation "hvbox(a break ∪ b)" left associative with precedence 50
+for @{ 'union $a $b }. (* \cup *)
+
+notation "hvbox({ term 19 a })" with precedence 90 for @{ 'singl $a}.
+
+notation "hvbox(a break \approx b)" non associative with precedence 45
+ for @{ 'napart $a $b}.
+
+notation "hvbox(a break # b)" non associative with precedence 45
+ for @{ 'apart $a $b}.
+
+notation "hvbox(a break \circ b)"
+ left associative with precedence 55
+for @{ 'compose $a $b }.
+
+notation < "↓ \ensp a" with precedence 55 for @{ 'downarrow $a }.
+notation > "↓ a" with precedence 55 for @{ 'downarrow $a }.
+
+notation "hvbox(U break ↓ V)" non associative with precedence 55 for @{ 'fintersects $U $V }.
+
+notation "↑a" with precedence 55 for @{ 'uparrow $a }.
+
+notation "hvbox(a break ↑ b)" with precedence 55 for @{ 'funion $a $b }.
+
+notation < "term 76 a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
+notation > "a \sup term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
+notation > "a ^ term 90 b" non associative with precedence 75 for @{ 'exp $a $b}.
+notation "s \sup (-1)" non associative with precedence 75 for @{ 'invert $s }.
+notation > "s ^ (-1)" non associative with precedence 75 for @{ 'invert $s }.
+notation < "s \sup (-1) x" non associative with precedence 90 for @{ 'invert_appl $s $x}.
+
+notation "| term 19 C |" with precedence 70 for @{ 'card $C }.
+
+notation "\naturals" non associative with precedence 90 for @{'N}.
+notation "\rationals" non associative with precedence 90 for @{'Q}.
+notation "\reals" non associative with precedence 90 for @{'R}.
+notation "\integers" non associative with precedence 90 for @{'Z}.
+notation "\complexes" non associative with precedence 90 for @{'C}.
+
+notation "\ee" with precedence 90 for @{ 'neutral }. (* ⅇ *)
+
+notation > "x ⊩ y" with precedence 45 for @{'Vdash2 $x $y ?}.
+notation > "x ⊩⎽ term 90 c y" with precedence 45 for @{'Vdash2 $x $y $c}.
+notation "x (⊩ \sub term 90 c) y" with precedence 45 for @{'Vdash2 $x $y $c}.
+notation > "⊩ " with precedence 60 for @{'Vdash ?}.
+notation "(⊩ \sub term 90 c) " with precedence 60 for @{'Vdash $c}.
+
+notation < "maction (mstyle color #ff0000 (…)) (t)"
+non associative with precedence 90 for @{'hide $t}.
--- /dev/null
+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).
\ No newline at end of file
--- /dev/null
+(*
+
+Notation for hint declaration
+==============================
+
+The idea is to write a context, with abstraction first, then
+recursive calls (let-in) and finally the two equivalent terms.
+The context can be empty. Note the ; to begin the second part of
+the context (necessary even if the first part is empty).
+
+ unification hint PREC \coloneq
+ ID : TY, ..., ID : TY
+ ; ID \equest T, ..., ID \equest T
+ \vdash T1 \equiv T2
+
+With unidoce and some ASCII art it looks like the following:
+
+ unification hint PREC ≔ ID : TY, ..., ID : TY;
+ ID ≟ T, ..., ID ≟ T
+ (*---------------------*) ⊢
+ T1 ≡ T2
+
+The order of premises is relevant, since they are processed in order
+(left to right).
+
+*)
+
+(* it seems unbelivable, but it works! *)
+notation > "≔ (list0 ( (list1 (ident x) sep , ) opt (: T) ) sep ,) opt (; (list1 (ident U ≟ term 19 V ) sep ,)) ⊢ term 19 Px ≡ term 19 Py"
+ with precedence 90
+ for @{ ${ fold right
+ @{ ${ default
+ @{ ${ fold right
+ @{ 'hint_decl $Px $Py }
+ rec acc1 @{ let ( ${ident U} : ?) ≝ $V in $acc1} } }
+ @{ 'hint_decl $Px $Py }
+ }
+ }
+ rec acc @{
+ ${ fold right @{ $acc } rec acc2
+ @{ ∀${ident x}:${ default @{ $T } @{ ? } }.$acc2 } }
+ }
+ }}.
+
+include "basics/pts.ma".
+
+definition hint_declaration_Type0 ≝ λA:Type[0] .λa,b:A.Prop.
+definition hint_declaration_Type1 ≝ λA:Type[1].λa,b:A.Prop.
+definition hint_declaration_Type2 ≝ λa,b:Type[2].Prop.
+definition hint_declaration_CProp0 ≝ λA:CProp[0].λa,b:A.Prop.
+definition hint_declaration_CProp1 ≝ λA:CProp[1].λa,b:A.Prop.
+definition hint_declaration_CProp2 ≝ λa,b:CProp[2].Prop.
+
+interpretation "hint_decl_Type2" 'hint_decl a b = (hint_declaration_Type2 a b).
+interpretation "hint_decl_CProp2" 'hint_decl a b = (hint_declaration_CProp2 a b).
+interpretation "hint_decl_Type1" 'hint_decl a b = (hint_declaration_Type1 ? a b).
+interpretation "hint_decl_CProp1" 'hint_decl a b = (hint_declaration_CProp1 ? a b).
+interpretation "hint_decl_CProp0" 'hint_decl a b = (hint_declaration_CProp0 ? a b).
+interpretation "hint_decl_Type0" 'hint_decl a b = (hint_declaration_Type0 ? a b).
+
+(* Non uniform coercions support
+record solution2 (S : Type[2]) (s : S) : Type[3] ≝ {
+ target2 : Type[2];
+ result2 : target2
+}.
+
+record solution1 (S : Type[1]) (s : S) : Type[2] ≝ {
+ target1 : Type[1];
+ result1 : target1
+}.
+
+coercion nonunifcoerc1 : ∀S:Type[1].∀s:S.∀l:solution1 S s. target1 S s l ≝ result1
+ on s : ? to target1 ???.
+
+coercion nonunifcoerc2 : ∀S:Type[2].∀s:S.∀l:solution2 S s. target2 S s l ≝ result2
+ on s : ? to target2 ???.
+*)
+
+(* Example of a non uniform coercion declaration
+
+ Type[0] setoid
+ >--->
+ MR R
+
+ provided MR = carr R
+
+unification hint 0 ≔ R : setoid;
+ MR ≟ carr R,
+ sol ≟ mk_solution1 Type[0] MR setoid R
+(* ---------------------------------------- *) ⊢
+ setoid ≡ target1 ? MR sol.
+
+*)
\ No newline at end of file
--- /dev/null
+include "basics/types.ma".
+include "basics/nat.ma".
+
+inductive list (A:Type[0]) : Type[0] :=
+ | nil: list A
+ | cons: A -> list A -> list A.
+
+notation "hvbox(hd break :: tl)"
+ right associative with precedence 47
+ for @{'cons $hd $tl}.
+
+notation "[ list0 x sep ; ]"
+ non associative with precedence 90
+ for ${fold right @'nil rec acc @{'cons $x $acc}}.
+
+notation "hvbox(l1 break @ l2)"
+ right associative with precedence 47
+ for @{'append $l1 $l2 }.
+
+interpretation "nil" 'nil = (nil ?).
+interpretation "cons" 'cons hd tl = (cons ? hd tl).
+
+definition not_nil: ∀A:Type[0].list A → Prop ≝
+ λA.λl.match l with [ nil ⇒ True | cons hd tl ⇒ False ].
+
+theorem nil_cons:
+ ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ [].
+ #A #l #a @nmk #Heq (change with (not_nil ? (a::l))) >Heq //
+qed.
+
+(*
+let rec id_list A (l: list A) on l :=
+ match l with
+ [ nil => []
+ | (cons hd tl) => hd :: id_list A tl ]. *)
+
+let rec append A (l1: list A) l2 on l1 ≝
+ match l1 with
+ [ nil ⇒ l2
+ | cons hd tl ⇒ hd :: append A tl l2 ].
+
+definition hd ≝ λA.λl: list A.λd:A.
+ match l with [ nil ⇒ d | cons a _ ⇒ a].
+
+definition tail ≝ λA.λl: list A.
+ match l with [ nil ⇒ [] | cons hd tl ⇒ tl].
+
+interpretation "append" 'append l1 l2 = (append ? l1 l2).
+
+theorem append_nil: ∀A.∀l:list A.l @ [] = l.
+#A #l (elim l) normalize // qed.
+
+theorem associative_append:
+ ∀A.associative (list A) (append A).
+#A #l1 #l2 #l3 (elim l1) normalize // qed.
+
+theorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
+#A #a #l #l1 >associative_append // qed.
+
+theorem nil_append_elim: ∀A.∀l1,l2: list A.∀P:?→?→Prop.
+ l1@l2=[] → P (nil A) (nil A) → P l1 l2.
+#A #l1 #l2 #P (cases l1) normalize //
+#a #l3 #heq destruct
+qed.
+
+theorem nil_to_nil: ∀A.∀l1,l2:list A.
+ l1@l2 = [] → l1 = [] ∧ l2 = [].
+#A #l1 #l2 #isnil @(nil_append_elim A l1 l2) /2/
+qed.
+
+(**************************** iterators ******************************)
+
+let rec map (A,B:Type[0]) (f: A → B) (l:list A) on l: list B ≝
+ match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)].
+
+lemma map_append : ∀A,B,f,l1,l2.
+ (map A B f l1) @ (map A B f l2) = map A B f (l1@l2).
+#A #B #f #l1 elim l1
+[ #l2 @refl
+| #h #t #IH #l2 normalize //
+] qed.
+
+let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:list A) on l :B ≝
+ match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
+
+definition filter ≝
+ λT.λp:T → bool.
+ foldr T (list T) (λx,l0.if p x then x::l0 else l0) (nil T).
+
+(* compose f [a1;...;an] [b1;...;bm] =
+ [f a1 b1; ... ;f an b1; ... ;f a1 bm; f an bm] *)
+
+definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2.
+ foldr ?? (λi,acc.(map ?? (f i) l2)@acc) [ ] l1.
+
+lemma filter_true : ∀A,l,a,p. p a = true →
+ filter A p (a::l) = a :: filter A p l.
+#A #l #a #p #pa (elim l) normalize >pa normalize // qed.
+
+lemma filter_false : ∀A,l,a,p. p a = false →
+ filter A p (a::l) = filter A p l.
+#A #l #a #p #pa (elim l) normalize >pa normalize // qed.
+
+theorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
+#A #B #f #g #l #eqfg (elim l) normalize // qed.
+
+(**************************** reverse *****************************)
+let rec rev_append S (l1,l2:list S) on l1 ≝
+ match l1 with
+ [ nil ⇒ l2
+ | cons a tl ⇒ rev_append S tl (a::l2)
+ ]
+.
+
+definition reverse ≝λS.λl.rev_append S l [].
+
+lemma reverse_single : ∀S,a. reverse S [a] = [a].
+// qed.
+
+lemma rev_append_def : ∀S,l1,l2.
+ rev_append S l1 l2 = (reverse S l1) @ l2 .
+#S #l1 elim l1 normalize //
+qed.
+
+lemma reverse_cons : ∀S,a,l. reverse S (a::l) = (reverse S l)@[a].
+#S #a #l whd in ⊢ (??%?); //
+qed.
+
+lemma reverse_append: ∀S,l1,l2.
+ reverse S (l1 @ l2) = (reverse S l2)@(reverse S l1).
+#S #l1 elim l1 [normalize // | #a #tl #Hind #l2 >reverse_cons
+>reverse_cons // qed.
+
+lemma reverse_reverse : ∀S,l. reverse S (reverse S l) = l.
+#S #l elim l // #a #tl #Hind >reverse_cons >reverse_append
+normalize // qed.
+
+(* an elimination principle for lists working on the tail;
+useful for strings *)
+lemma list_elim_left: ∀S.∀P:list S → Prop. P (nil S) →
+(∀a.∀tl.P tl → P (tl@[a])) → ∀l. P l.
+#S #P #Pnil #Pstep #l <(reverse_reverse … l)
+generalize in match (reverse S l); #l elim l //
+#a #tl #H >reverse_cons @Pstep //
+qed.
+
+(**************************** length ******************************)
+
+let rec length (A:Type[0]) (l:list A) on l ≝
+ match l with
+ [ nil ⇒ O
+ | cons a tl ⇒ S (length A tl)].
+
+notation "|M|" non associative with precedence 60 for @{'norm $M}.
+interpretation "norm" 'norm l = (length ? l).
+
+lemma length_append: ∀A.∀l1,l2:list A.
+ |l1@l2| = |l1|+|l2|.
+#A #l1 elim l1 // normalize /2/
+qed.
+
+(****************************** nth ********************************)
+let rec nth n (A:Type[0]) (l:list A) (d:A) ≝
+ match n with
+ [O ⇒ hd A l d
+ |S m ⇒ nth m A (tail A l) d].
+
+lemma nth_nil: ∀A,a,i. nth i A ([]) a = a.
+#A #a #i elim i normalize //
+qed.
+
+(****************************** nth_opt ********************************)
+let rec nth_opt (A:Type[0]) (n:nat) (l:list A) on l : option A ≝
+match l with
+[ nil ⇒ None ?
+| cons h t ⇒ match n with [ O ⇒ Some ? h | S m ⇒ nth_opt A m t ]
+].
+
+(**************************** All *******************************)
+
+let rec All (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
+match l with
+[ nil ⇒ True
+| cons h t ⇒ P h ∧ All A P t
+].
+
+lemma All_mp : ∀A,P,Q. (∀a.P a → Q a) → ∀l. All A P l → All A Q l.
+#A #P #Q #H #l elim l normalize //
+#h #t #IH * /3/
+qed.
+
+lemma All_nth : ∀A,P,n,l.
+ All A P l →
+ ∀a.
+ nth_opt A n l = Some A a →
+ P a.
+#A #P #n elim n
+[ * [ #_ #a #E whd in E:(??%?); destruct
+ | #hd #tl * #H #_ #a #E whd in E:(??%?); destruct @H
+ ]
+| #m #IH *
+ [ #_ #a #E whd in E:(??%?); destruct
+ | #hd #tl * #_ whd in ⊢ (? → ∀_.??%? → ?); @IH
+ ]
+] qed.
+
+(**************************** Exists *******************************)
+
+let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
+match l with
+[ nil ⇒ False
+| cons h t ⇒ (P h) ∨ (Exists A P t)
+].
+
+lemma Exists_append : ∀A,P,l1,l2.
+ Exists A P (l1 @ l2) → Exists A P l1 ∨ Exists A P l2.
+#A #P #l1 elim l1
+[ normalize /2/
+| #h #t #IH #l2 *
+ [ #H /3/
+ | #H cases (IH l2 H) /3/
+ ]
+] qed.
+
+lemma Exists_append_l : ∀A,P,l1,l2.
+ Exists A P l1 → Exists A P (l1@l2).
+#A #P #l1 #l2 elim l1
+[ *
+| #h #t #IH *
+ [ #H %1 @H
+ | #H %2 @IH @H
+ ]
+] qed.
+
+lemma Exists_append_r : ∀A,P,l1,l2.
+ Exists A P l2 → Exists A P (l1@l2).
+#A #P #l1 #l2 elim l1
+[ #H @H
+| #h #t #IH #H %2 @IH @H
+] qed.
+
+lemma Exists_add : ∀A,P,l1,x,l2. Exists A P (l1@l2) → Exists A P (l1@x::l2).
+#A #P #l1 #x #l2 elim l1
+[ normalize #H %2 @H
+| #h #t #IH normalize * [ #H %1 @H | #H %2 @IH @H ]
+qed.
+
+lemma Exists_mid : ∀A,P,l1,x,l2. P x → Exists A P (l1@x::l2).
+#A #P #l1 #x #l2 #H elim l1
+[ %1 @H
+| #h #t #IH %2 @IH
+] qed.
+
+lemma Exists_map : ∀A,B,P,Q,f,l.
+Exists A P l →
+(∀a.P a → Q (f a)) →
+Exists B Q (map A B f l).
+#A #B #P #Q #f #l elim l //
+#h #t #IH * [ #H #F %1 @F @H | #H #F %2 @IH [ @H | @F ] ] qed.
+
+lemma Exists_All : ∀A,P,Q,l.
+ Exists A P l →
+ All A Q l →
+ ∃x. P x ∧ Q x.
+#A #P #Q #l elim l [ * | #hd #tl #IH * [ #H1 * #H2 #_ %{hd} /2/ | #H1 * #_ #H2 @IH // ]
+qed.
+
+(**************************** fold *******************************)
+
+let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→bool) (f:A→B) (l:list A) on l :B ≝
+ match l with
+ [ nil ⇒ b
+ | cons a l ⇒
+ if p a then op (f a) (fold A B op b p f l)
+ else fold A B op b p f l].
+
+notation "\fold [ op , nil ]_{ ident i ∈ l | p} f"
+ with precedence 80
+for @{'fold $op $nil (λ${ident i}. $p) (λ${ident i}. $f) $l}.
+
+notation "\fold [ op , nil ]_{ident i ∈ l } f"
+ with precedence 80
+for @{'fold $op $nil (λ${ident i}.true) (λ${ident i}. $f) $l}.
+
+interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l).
+
+theorem fold_true:
+∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a = true →
+ \fold[op,nil]_{i ∈ a::l| p i} (f i) =
+ op (f a) \fold[op,nil]_{i ∈ l| p i} (f i).
+#A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
+
+theorem fold_false:
+∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f.
+p a = false → \fold[op,nil]_{i ∈ a::l| p i} (f i) =
+ \fold[op,nil]_{i ∈ l| p i} (f i).
+#A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
+
+theorem fold_filter:
+∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B.
+ \fold[op,nil]_{i ∈ l| p i} (f i) =
+ \fold[op,nil]_{i ∈ (filter A p l)} (f i).
+#A #B #a #l #p #op #nil #f elim l //
+#a #tl #Hind cases(true_or_false (p a)) #pa
+ [ >filter_true // > fold_true // >fold_true //
+ | >filter_false // >fold_false // ]
+qed.
+
+record Aop (A:Type[0]) (nil:A) : Type[0] ≝
+ {op :2> A → A → A;
+ nill:∀a. op nil a = a;
+ nilr:∀a. op a nil = a;
+ assoc: ∀a,b,c.op a (op b c) = op (op a b) c
+ }.
+
+theorem fold_sum: ∀A,B. ∀I,J:list A.∀nil.∀op:Aop B nil.∀f.
+ op (\fold[op,nil]_{i∈I} (f i)) (\fold[op,nil]_{i∈J} (f i)) =
+ \fold[op,nil]_{i∈(I@J)} (f i).
+#A #B #I #J #nil #op #f (elim I) normalize
+ [>nill //|#a #tl #Hind <assoc //]
+qed.
+
--- /dev/null
+(* boolean functions over lists *)
+
+include "basics/list.ma".
+include "basics/sets.ma".
+include "basics/deqsets.ma".
+
+(********* search *********)
+
+let rec memb (S:DeqSet) (x:S) (l: list S) on l ≝
+ match l with
+ [ nil ⇒ false
+ | cons a tl ⇒ (x == a) ∨ memb S x tl
+ ].
+
+notation < "\memb x l" non associative with precedence 90 for @{'memb $x $l}.
+interpretation "boolean membership" 'memb a l = (memb ? a l).
+
+lemma memb_hd: ∀S,a,l. memb S a (a::l) = true.
+#S #a #l normalize >(proj2 … (eqb_true S …) (refl S a)) //
+qed.
+
+lemma memb_cons: ∀S,a,b,l.
+ memb S a l = true → memb S a (b::l) = true.
+#S #a #b #l normalize cases (a==b) normalize //
+qed.
+
+lemma memb_single: ∀S,a,x. memb S a [x] = true → a = x.
+#S #a #x normalize cases (true_or_false … (a==x)) #H
+ [#_ >(\P H) // |>H normalize #abs @False_ind /2/]
+qed.
+
+lemma memb_append: ∀S,a,l1,l2.
+memb S a (l1@l2) = true →
+ memb S a l1= true ∨ memb S a l2 = true.
+#S #a #l1 elim l1 normalize [#l2 #H %2 //]
+#b #tl #Hind #l2 cases (a==b) normalize /2/
+qed.
+
+lemma memb_append_l1: ∀S,a,l1,l2.
+ memb S a l1= true → memb S a (l1@l2) = true.
+#S #a #l1 elim l1 normalize
+ [normalize #le #abs @False_ind /2/
+ |#b #tl #Hind #l2 cases (a==b) normalize /2/
+ ]
+qed.
+
+lemma memb_append_l2: ∀S,a,l1,l2.
+ memb S a l2= true → memb S a (l1@l2) = true.
+#S #a #l1 elim l1 normalize //
+#b #tl #Hind #l2 cases (a==b) normalize /2/
+qed.
+
+lemma memb_exists: ∀S,a,l.memb S a l = true →
+ ∃l1,l2.l=l1@(a::l2).
+#S #a #l elim l [normalize #abs @False_ind /2/]
+#b #tl #Hind #H cases (orb_true_l … H)
+ [#eqba @(ex_intro … (nil S)) @(ex_intro … tl) >(\P eqba) //
+ |#mem_tl cases (Hind mem_tl) #l1 * #l2 #eqtl
+ @(ex_intro … (b::l1)) @(ex_intro … l2) >eqtl //
+ ]
+qed.
+
+lemma not_memb_to_not_eq: ∀S,a,b,l.
+ memb S a l = false → memb S b l = true → a==b = false.
+#S #a #b #l cases (true_or_false (a==b)) //
+#eqab >(\P eqab) #H >H #abs @False_ind /2/
+qed.
+
+lemma memb_map: ∀S1,S2,f,a,l. memb S1 a l= true →
+ memb S2 (f a) (map … f l) = true.
+#S1 #S2 #f #a #l elim l normalize [//]
+#x #tl #memba cases (true_or_false (a==x))
+ [#eqx >eqx >(\P eqx) >(\b (refl … (f x))) normalize //
+ |#eqx >eqx cases (f a==f x) normalize /2/
+ ]
+qed.
+
+lemma memb_compose: ∀S1,S2,S3,op,a1,a2,l1,l2.
+ memb S1 a1 l1 = true → memb S2 a2 l2 = true →
+ memb S3 (op a1 a2) (compose S1 S2 S3 op l1 l2) = true.
+#S1 #S2 #S3 #op #a1 #a2 #l1 elim l1 [normalize //]
+#x #tl #Hind #l2 #memba1 #memba2 cases (orb_true_l … memba1)
+ [#eqa1 >(\P eqa1) @memb_append_l1 @memb_map //
+ |#membtl @memb_append_l2 @Hind //
+ ]
+qed.
+
+(**************** unicity test *****************)
+
+let rec uniqueb (S:DeqSet) l on l : bool ≝
+ match l with
+ [ nil ⇒ true
+ | cons a tl ⇒ notb (memb S a tl) ∧ uniqueb S tl
+ ].
+
+(* unique_append l1 l2 add l1 in fornt of l2, but preserving unicity *)
+
+let rec unique_append (S:DeqSet) (l1,l2: list S) on l1 ≝
+ match l1 with
+ [ nil ⇒ l2
+ | cons a tl ⇒
+ let r ≝ unique_append S tl l2 in
+ if memb S a r then r else a::r
+ ].
+
+axiom unique_append_elim: ∀S:DeqSet.∀P: S → Prop.∀l1,l2.
+(∀x. memb S x l1 = true → P x) → (∀x. memb S x l2 = true → P x) →
+∀x. memb S x (unique_append S l1 l2) = true → P x.
+
+lemma unique_append_unique: ∀S,l1,l2. uniqueb S l2 = true →
+ uniqueb S (unique_append S l1 l2) = true.
+#S #l1 elim l1 normalize // #a #tl #Hind #l2 #uniquel2
+cases (true_or_false … (memb S a (unique_append S tl l2)))
+#H >H normalize [@Hind //] >H normalize @Hind //
+qed.
+
+(******************* sublist *******************)
+definition sublist ≝
+ λS,l1,l2.∀a. memb S a l1 = true → memb S a l2 = true.
+
+lemma sublist_length: ∀S,l1,l2.
+ uniqueb S l1 = true → sublist S l1 l2 → |l1| ≤ |l2|.
+#S #l1 elim l1 //
+#a #tl #Hind #l2 #unique #sub
+cut (∃l3,l4.l2=l3@(a::l4)) [@memb_exists @sub //]
+* #l3 * #l4 #eql2 >eql2 >length_append normalize
+applyS le_S_S <length_append @Hind [@(andb_true_r … unique)]
+>eql2 in sub; #sub #x #membx
+cases (memb_append … (sub x (orb_true_r2 … membx)))
+ [#membxl3 @memb_append_l1 //
+ |#membxal4 cases (orb_true_l … membxal4)
+ [#eqxa @False_ind lapply (andb_true_l … unique)
+ <(\P eqxa) >membx normalize /2/ |#membxl4 @memb_append_l2 //
+ ]
+ ]
+qed.
+
+lemma sublist_unique_append_l1:
+ ∀S,l1,l2. sublist S l1 (unique_append S l1 l2).
+#S #l1 elim l1 normalize [#l2 #S #abs @False_ind /2/]
+#x #tl #Hind #l2 #a
+normalize cases (true_or_false … (a==x)) #eqax >eqax
+[<(\P eqax) cases (true_or_false (memb S a (unique_append S tl l2)))
+ [#H >H normalize // | #H >H normalize >(\b (refl … a)) //]
+|cases (memb S x (unique_append S tl l2)) normalize
+ [/2/ |>eqax normalize /2/]
+]
+qed.
+
+lemma sublist_unique_append_l2:
+ ∀S,l1,l2. sublist S l2 (unique_append S l1 l2).
+#S #l1 elim l1 [normalize //] #x #tl #Hind normalize
+#l2 #a cases (memb S x (unique_append S tl l2)) normalize
+[@Hind | cases (a==x) normalize // @Hind]
+qed.
+
+lemma decidable_sublist:∀S,l1,l2.
+ (sublist S l1 l2) ∨ ¬(sublist S l1 l2).
+#S #l1 #l2 elim l1
+ [%1 #a normalize in ⊢ (%→?); #abs @False_ind /2/
+ |#a #tl * #subtl
+ [cases (true_or_false (memb S a l2)) #memba
+ [%1 whd #x #membx cases (orb_true_l … membx)
+ [#eqax >(\P eqax) // |@subtl]
+ |%2 @(not_to_not … (eqnot_to_noteq … true memba)) #H1 @H1 @memb_hd
+ ]
+ |%2 @(not_to_not … subtl) #H1 #x #H2 @H1 @memb_cons //
+ ]
+ ]
+qed.
+
+(********************* filtering *****************)
+
+lemma filter_true: ∀S,f,a,l.
+ memb S a (filter S f l) = true → f a = true.
+#S #f #a #l elim l [normalize #H @False_ind /2/]
+#b #tl #Hind cases (true_or_false (f b)) #H
+normalize >H normalize [2:@Hind]
+cases (true_or_false (a==b)) #eqab
+ [#_ >(\P eqab) // | >eqab normalize @Hind]
+qed.
+
+lemma memb_filter_memb: ∀S,f,a,l.
+ memb S a (filter S f l) = true → memb S a l = true.
+#S #f #a #l elim l [normalize //]
+#b #tl #Hind normalize (cases (f b)) normalize
+cases (a==b) normalize // @Hind
+qed.
+
+lemma memb_filter: ∀S,f,l,x. memb S x (filter ? f l) = true →
+memb S x l = true ∧ (f x = true).
+/3/ qed.
+
+lemma memb_filter_l: ∀S,f,x,l. (f x = true) → memb S x l = true →
+memb S x (filter ? f l) = true.
+#S #f #x #l #fx elim l normalize //
+#b #tl #Hind cases (true_or_false (x==b)) #eqxb
+ [<(\P eqxb) >(\b (refl … x)) >fx normalize >(\b (refl … x)) normalize //
+ |>eqxb cases (f b) normalize [>eqxb normalize @Hind| @Hind]
+ ]
+qed.
+
+(********************* exists *****************)
+
+let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : bool ≝
+match l with
+[ nil ⇒ false
+| cons h t ⇒ orb (p h) (exists A p t)
+].
+
+lemma Exists_exists : ∀A,P,l.
+ Exists A P l →
+ ∃x. P x.
+#A #P #l elim l [ * | #hd #tl #IH * [ #H %{hd} @H | @IH ]
+qed.
--- /dev/null
+include "basics/pts.ma".
+include "basics/hints_declaration.ma".
+
+(* propositional equality *)
+
+inductive eq (A:Type[2]) (x:A) : A → Prop ≝
+ refl: eq A x x.
+
+interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
+interpretation "leibniz reflexivity" 'refl = refl.
+
+lemma eq_rect_r:
+ ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[3]. P a (refl A a) → P x p.
+ #A #a #x #p (cases p) // qed.
+
+lemma eq_ind_r :
+ ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+ #A #a #P #p #x0 #p0; @(eq_rect_r ? ? ? p0) //; qed.
+
+lemma eq_rect_Type0_r:
+ ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+ #A #a #P #H #x #p lapply H lapply P
+ cases p; //; qed.
+
+lemma eq_rect_Type1_r:
+ ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+ #A #a #P #H #x #p lapply H lapply P
+ cases p; //; qed.
+
+lemma eq_rect_Type2_r:
+ ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+ #A #a #P #H #x #p lapply H lapply P
+ cases p; //; qed.
+
+lemma eq_rect_Type3_r:
+ ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[3]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+ #A #a #P #H #x #p lapply H lapply P
+ cases p; //; qed.
+
+theorem rewrite_l: ∀A:Type[2].∀x.∀P:A → Type[2]. P x → ∀y. x = y → P y.
+#A #x #P #Hx #y #Heq (cases Heq); //; qed.
+
+theorem sym_eq: ∀A.∀x,y:A. x = y → y = x.
+#A #x #y #Heq @(rewrite_l A x (λz.z=x)) // qed.
+
+theorem rewrite_r: ∀A:Type[2].∀x.∀P:A → Type[2]. P x → ∀y. y = x → P y.
+#A #x #P #Hx #y #Heq (cases (sym_eq ? ? ? Heq)); //; qed.
+
+theorem eq_coerc: ∀A,B:Type[0].A→(A=B)→B.
+#A #B #Ha #Heq (elim Heq); //; qed.
+
+theorem trans_eq : ∀A.∀x,y,z:A. x = y → y = z → x = z.
+#A #x #y #z #H1 #H2 >H1; //; qed.
+
+theorem eq_f: ∀A,B.∀f:A→B.∀x,y:A. x=y → f x = f y.
+#A #B #f #x #y #H >H; //; qed.
+
+(* deleterio per auto? *)
+theorem eq_f2: ∀A,B,C.∀f:A→B→C.
+∀x1,x2:A.∀y1,y2:B. x1=x2 → y1=y2 → f x1 y1 = f x2 y2.
+#A #B #C #f #x1 #x2 #y1 #y2 #E1 #E2 >E1; >E2; //; qed.
+
+lemma eq_f3: ∀A,B,C,D.∀f:A→B→C->D.
+∀x1,x2:A.∀y1,y2:B. ∀z1,z2:C. x1=x2 → y1=y2 → z1=z2 → f x1 y1 z1 = f x2 y2 z2.
+#A #B #C #D #f #x1 #x2 #y1 #y2 #z1 #z2 #E1 #E2 #E3 >E1; >E2; >E3 //; qed.
+
+(* hint to genereric equality
+definition eq_equality: equality ≝
+ mk_equality eq refl rewrite_l rewrite_r.
+
+
+unification hint 0 ≔ T,a,b;
+ X ≟ eq_equality
+(*------------------------------------*) ⊢
+ equal X T a b ≡ eq T a b.
+*)
+
+(********** connectives ********)
+
+inductive True: Prop ≝
+I : True.
+
+inductive False: Prop ≝ .
+
+(* ndefinition Not: Prop → Prop ≝
+λA. A → False. *)
+
+inductive Not (A:Prop): Prop ≝
+nmk: (A → False) → Not A.
+
+interpretation "logical not" 'not x = (Not x).
+
+theorem absurd : ∀A:Prop. A → ¬A → False.
+#A #H #Hn (elim Hn); /2/; qed.
+
+(*
+ntheorem absurd : ∀ A,C:Prop. A → ¬A → C.
+#A; #C; #H; #Hn; nelim (Hn H).
+nqed. *)
+
+theorem not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A.
+/4/; qed.
+
+(* inequality *)
+interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
+
+theorem sym_not_eq: ∀A.∀x,y:A. x ≠ y → y ≠ x.
+/3/; qed.
+
+(* and *)
+inductive And (A,B:Prop) : Prop ≝
+ conj : A → B → And A B.
+
+interpretation "logical and" 'and x y = (And x y).
+
+theorem proj1: ∀A,B:Prop. A ∧ B → A.
+#A #B #AB (elim AB) //; qed.
+
+theorem proj2: ∀ A,B:Prop. A ∧ B → B.
+#A #B #AB (elim AB) //; qed.
+
+(* or *)
+inductive Or (A,B:Prop) : Prop ≝
+ or_introl : A → (Or A B)
+ | or_intror : B → (Or A B).
+
+interpretation "logical or" 'or x y = (Or x y).
+
+definition decidable : Prop → Prop ≝
+λ A:Prop. A ∨ ¬ A.
+
+(* exists *)
+inductive ex (A:Type[0]) (P:A → Prop) : Prop ≝
+ ex_intro: ∀ x:A. P x → ex A P.
+
+interpretation "exists" 'exists x = (ex ? x).
+
+inductive ex2 (A:Type[0]) (P,Q:A →Prop) : Prop ≝
+ ex_intro2: ∀ x:A. P x → Q x → ex2 A P Q.
+
+(* iff *)
+definition iff :=
+ λ A,B. (A → B) ∧ (B → A).
+
+interpretation "iff" 'iff a b = (iff a b).
+
+lemma iff_sym: ∀A,B. A ↔ B → B ↔ A.
+#A #B * /3/ qed.
+
+lemma iff_trans:∀A,B,C. A ↔ B → B ↔ C → A ↔ C.
+#A #B #C * #H1 #H2 * #H3 #H4 % /3/ qed.
+
+lemma iff_not: ∀A,B. A ↔ B → ¬A ↔ ¬B.
+#A #B * #H1 #H2 % /3/ qed.
+
+lemma iff_and_l: ∀A,B,C. A ↔ B → C ∧ A ↔ C ∧ B.
+#A #B #C * #H1 #H2 % * /3/ qed.
+
+lemma iff_and_r: ∀A,B,C. A ↔ B → A ∧ C ↔ B ∧ C.
+#A #B #C * #H1 #H2 % * /3/ qed.
+
+lemma iff_or_l: ∀A,B,C. A ↔ B → C ∨ A ↔ C ∨ B.
+#A #B #C * #H1 #H2 % * /3/ qed.
+
+lemma iff_or_r: ∀A,B,C. A ↔ B → A ∨ C ↔ B ∨ C.
+#A #B #C * #H1 #H2 % * /3/ qed.
+
+(* cose per destruct: da rivedere *)
+
+definition R0 ≝ λT:Type[0].λt:T.t.
+
+definition R1 ≝ eq_rect_Type0.
+
+(* used for lambda-delta *)
+definition R2 :
+ ∀T0:Type[0].
+ ∀a0:T0.
+ ∀T1:∀x0:T0. a0=x0 → Type[0].
+ ∀a1:T1 a0 (refl ? a0).
+ ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
+ ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
+ ∀b0:T0.
+ ∀e0:a0 = b0.
+ ∀b1: T1 b0 e0.
+ ∀e1:R1 ?? T1 a1 ? e0 = b1.
+ T2 b0 e0 b1 e1.
+#T0 #a0 #T1 #a1 #T2 #a2 #b0 #e0 #b1 #e1
+@(eq_rect_Type0 ????? e1)
+@(R1 ?? ? ?? e0)
+@a2
+qed.
+
+definition R3 :
+ ∀T0:Type[0].
+ ∀a0:T0.
+ ∀T1:∀x0:T0. a0=x0 → Type[0].
+ ∀a1:T1 a0 (refl ? a0).
+ ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
+ ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
+ ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
+ ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
+ ∀a3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).
+ ∀b0:T0.
+ ∀e0:a0 = b0.
+ ∀b1: T1 b0 e0.
+ ∀e1:R1 ?? T1 a1 ? e0 = b1.
+ ∀b2: T2 b0 e0 b1 e1.
+ ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
+ T3 b0 e0 b1 e1 b2 e2.
+#T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #b0 #e0 #b1 #e1 #b2 #e2
+@(eq_rect_Type0 ????? e2)
+@(R2 ?? ? ???? e0 ? e1)
+@a3
+qed.
+
+definition R4 :
+ ∀T0:Type[0].
+ ∀a0:T0.
+ ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
+ ∀a1:T1 a0 (refl T0 a0).
+ ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
+ ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1).
+ ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
+ ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
+ ∀a3:T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
+ a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2).
+ ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
+ ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
+ ∀x3:T3 x0 p0 x1 p1 x2 p2.∀p3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 x0 p0 x1 p1 x2 p2) x3.
+ Type[0].
+ ∀a4:T4 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
+ a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2)
+ a3 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
+ a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2))
+ a3).
+ ∀b0:T0.
+ ∀e0:eq (T0 …) a0 b0.
+ ∀b1: T1 b0 e0.
+ ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
+ ∀b2: T2 b0 e0 b1 e1.
+ ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
+ ∀b3: T3 b0 e0 b1 e1 b2 e2.
+ ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
+ T4 b0 e0 b1 e1 b2 e2 b3 e3.
+#T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #T4 #a4 #b0 #e0 #b1 #e1 #b2 #e2 #b3 #e3
+@(eq_rect_Type0 ????? e3)
+@(R3 ????????? e0 ? e1 ? e2)
+@a4
+qed.
+
+definition eqProp ≝ λA:Prop.eq A.
+
+(* Example to avoid indexing and the consequential creation of ill typed
+ terms during paramodulation *)
+example lemmaK : ∀A.∀x:A.∀h:x=x. eqProp ? h (refl A x).
+#A #x #h @(refl ? h: eqProp ? ? ?).
+qed.
+
+theorem streicherK : ∀T:Type[2].∀t:T.∀P:t = t → Type[3].P (refl ? t) → ∀p.P p.
+ #T #t #P #H #p >(lemmaK T t p) @H
+qed.
--- /dev/null
+include "basics/relations.ma".
+include "basics/bool.ma".
+
+(* natural numbers *)
+
+inductive nat : Type[0] ≝
+ | O : nat
+ | S : nat → nat.
+
+interpretation "Natural numbers" 'N = nat.
+
+alias num (instance 0) = "natural number".
+
+definition pred ≝
+ λn. match n with [ O ⇒ O | S p ⇒ p].
+
+definition not_zero: nat → Prop ≝
+ λn: nat. match n with [ O ⇒ False | (S p) ⇒ True ].
+
+(* order relations *)
+
+inductive le (n:nat) : nat → Prop ≝
+ | le_n : le n n
+ | le_S : ∀ m:nat. le n m → le n (S m).
+
+interpretation "natural 'less or equal to'" 'leq x y = (le x y).
+
+interpretation "natural 'neither less nor equal to'" 'nleq x y = (Not (le x y)).
+
+definition lt: nat → nat → Prop ≝ λn,m. S n ≤ m.
+
+interpretation "natural 'less than'" 'lt x y = (lt x y).
+
+interpretation "natural 'not less than'" 'nless x y = (Not (lt x y)).
+
+(* abstract properties *)
+
+definition increasing ≝ λf:nat → nat. ∀n:nat. f n < f (S n).
+
+(* arithmetic operations *)
+
+let rec plus n m ≝
+ match n with [ O ⇒ m | S p ⇒ S (plus p m) ].
+
+interpretation "natural plus" 'plus x y = (plus x y).
+
+(* Generic conclusion ******************************************************)
+
+theorem nat_case:
+ ∀n:nat.∀P:nat → Prop.
+ (n=O → P O) → (∀m:nat. n= S m → P (S m)) → P n.
+#n #P (elim n) /2/ qed.
+
+theorem nat_elim2 :
+ ∀R:nat → nat → Prop.
+ (∀n:nat. R O n)
+ → (∀n:nat. R (S n) O)
+ → (∀n,m:nat. R n m → R (S n) (S m))
+ → ∀n,m:nat. R n m.
+#R #ROn #RSO #RSS #n (elim n) // #n0 #Rn0m #m (cases m) /2/ qed.
+
+lemma le_gen: ∀P:nat → Prop.∀n.(∀i. i ≤ n → P i) → P n.
+/2/ qed.
+
+(* Equalities ***************************************************************)
+
+theorem pred_Sn : ∀n. n = pred (S n).
+// qed.
+
+theorem injective_S : injective nat nat S.
+#a #b #H >(pred_Sn a) >(pred_Sn b) @eq_f // qed.
+
+theorem S_pred: ∀n. O < n → S(pred n) = n.
+#n #posn (cases posn) //
+qed.
+
+theorem plus_O_n: ∀n:nat. n = O + n.
+// qed.
+
+theorem plus_n_O: ∀n:nat. n = n + O.
+#n (elim n) normalize // qed.
+
+theorem plus_n_Sm : ∀n,m:nat. S (n+m) = n + S m.
+#n (elim n) normalize // qed.
+
+theorem commutative_plus: commutative ? plus.
+#n (elim n) normalize // qed.
+
+theorem associative_plus : associative nat plus.
+#n (elim n) normalize // qed.
+
+theorem assoc_plus1: ∀a,b,c. c + (b + a) = b + c + a.
+// qed.
+
+theorem injective_plus_r: ∀n:nat.injective nat nat (λm.n+m).
+#n (elim n) normalize /3/ qed.
+
+theorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m.
+/2/ qed.
+
+(* not_zero *)
+
+theorem lt_to_not_zero : ∀n,m:nat. n < m → not_zero m.
+#n #m #Hlt (elim Hlt) // qed.
+
+(* le *)
+
+theorem le_S_S: ∀n,m:nat. n ≤ m → S n ≤ S m.
+#n #m #lenm (elim lenm) /2/ qed.
+
+theorem le_O_n : ∀n:nat. O ≤ n.
+#n (elim n) /2/ qed.
+
+theorem le_n_Sn : ∀n:nat. n ≤ S n.
+/2/ qed.
+
+theorem transitive_le : transitive nat le.
+#a #b #c #leab #lebc (elim lebc) /2/
+qed.
+
+theorem le_pred_n : ∀n:nat. pred n ≤ n.
+#n (elim n) // qed.
+
+theorem monotonic_pred: monotonic ? le pred.
+#n #m #lenm (elim lenm) /2/ qed.
+
+theorem le_S_S_to_le: ∀n,m:nat. S n ≤ S m → n ≤ m.
+(* demo *)
+/2/ qed-.
+
+theorem monotonic_le_plus_r:
+∀n:nat.monotonic nat le (λm.n + m).
+#n #a #b (elim n) normalize //
+#m #H #leab @le_S_S /2/ qed.
+
+theorem monotonic_le_plus_l:
+∀m:nat.monotonic nat le (λn.n + m).
+/2/ qed.
+
+theorem le_plus: ∀n1,n2,m1,m2:nat. n1 ≤ n2 → m1 ≤ m2
+→ n1 + m1 ≤ n2 + m2.
+#n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1+m2))
+/2/ qed-.
+
+theorem le_plus_n :∀n,m:nat. m ≤ n + m.
+/2/ qed.
+
+lemma le_plus_a: ∀a,n,m. n ≤ m → n ≤ a + m.
+/2/ qed.
+
+lemma le_plus_b: ∀b,n,m. n + b ≤ m → n ≤ m.
+/2/ qed.
+
+theorem le_plus_n_r :∀n,m:nat. m ≤ m + n.
+/2/ qed.
+
+theorem eq_plus_to_le: ∀n,m,p:nat.n=m+p → m ≤ n.
+// qed-.
+
+theorem le_plus_to_le: ∀a,n,m. a + n ≤ a + m → n ≤ m.
+#a (elim a) normalize /3/ qed.
+
+theorem le_plus_to_le_r: ∀a,n,m. n + a ≤ m +a → n ≤ m.
+/2/ qed-.
+
+(* lt *)
+
+theorem transitive_lt: transitive nat lt.
+#a #b #c #ltab #ltbc (elim ltbc) /2/
+qed.
+
+theorem lt_to_le_to_lt: ∀n,m,p:nat. n < m → m ≤ p → n < p.
+#n #m #p #H #H1 (elim H1) /2/ qed.
+
+theorem le_to_lt_to_lt: ∀n,m,p:nat. n ≤ m → m < p → n < p.
+#n #m #p #H (elim H) /3/ qed.
+
+theorem lt_S_to_lt: ∀n,m. S n < m → n < m.
+/2/ qed.
+
+theorem ltn_to_ltO: ∀n,m:nat. n < m → O < m.
+/2/ qed.
+
+theorem lt_O_S : ∀n:nat. O < S n.
+/2/ qed.
+
+theorem monotonic_lt_plus_r:
+∀n:nat.monotonic nat lt (λm.n+m).
+/2/ qed.
+
+theorem monotonic_lt_plus_l:
+∀n:nat.monotonic nat lt (λm.m+n).
+/2/ qed.
+
+theorem lt_plus: ∀n,m,p,q:nat. n < m → p < q → n + p < m + q.
+#n #m #p #q #ltnm #ltpq
+@(transitive_lt ? (n+q))/2/ qed.
+
+theorem lt_plus_to_lt_l :∀n,p,q:nat. p+n < q+n → p<q.
+/2/ qed.
+
+theorem lt_plus_to_lt_r :∀n,p,q:nat. n+p < n+q → p<q.
+/2/ qed-.
+
+theorem increasing_to_monotonic: ∀f:nat → nat.
+ increasing f → monotonic nat lt f.
+#f #incr #n #m #ltnm (elim ltnm) /2/
+qed.
+
+(* not le, lt *)
+
+theorem not_le_Sn_O: ∀ n:nat. S n ≰ O.
+#n @nmk #Hlen0 @(lt_to_not_zero ?? Hlen0) qed.
+
+theorem not_le_to_not_le_S_S: ∀ n,m:nat. n ≰ m → S n ≰ S m.
+/3/ qed.
+
+theorem not_le_S_S_to_not_le: ∀ n,m:nat. S n ≰ S m → n ≰ m.
+/3/ qed.
+
+theorem not_le_Sn_n: ∀n:nat. S n ≰ n.
+#n (elim n) /2/ qed.
+
+theorem lt_to_not_le: ∀n,m. n < m → m ≰ n.
+#n #m #Hltnm (elim Hltnm) /3/ qed.
+
+theorem not_le_to_lt: ∀n,m. n ≰ m → m < n.
+@nat_elim2 #n
+ [#abs @False_ind /2/
+ |/2/
+ |#m #Hind #HnotleSS @le_S_S /3/
+ ]
+qed.
+
+(* not lt, le *)
+
+theorem not_lt_to_le: ∀n,m:nat. n ≮ m → m ≤ n.
+/4/ qed.
+
+theorem le_to_not_lt: ∀n,m:nat. n ≤ m → m ≮ n.
+#n #m #H @lt_to_not_le /2/ (* /3/ *) qed.
+
+(*********************** boolean arithmetics ********************)
+
+
+let rec eqbnat n m ≝
+match n with
+ [ O ⇒ match m with [ O ⇒ true | S q ⇒ false]
+ | S p ⇒ match m with [ O ⇒ false | S q ⇒ eqbnat p q]
+ ].
+
+theorem eqbnat_elim : ∀ n,m:nat.∀ P:bool → Prop.
+(n=m → (P true)) → (n ≠ m → (P false)) → (P (eqbnat n m)).
+@nat_elim2
+ [#n (cases n) normalize /3/
+ |normalize /3/
+ |normalize /4/
+ ]
+qed.
+
+theorem eqbnat_n_n: ∀n. eqbnat n n = true.
+#n (elim n) normalize // qed.
+
+theorem eqbnat_true_to_eq: ∀n,m:nat. eqbnat n m = true → n = m.
+#n #m @(eqbnat_elim n m) // #_ #abs @False_ind /2/ qed.
+
+(* theorem eqb_false_to_not_eq: ∀n,m:nat. eqbnat n m = false → n ≠ m.
+#n #m @(eqbnat_elim n m) /2/ qed. *)
+
+theorem eq_to_eqbnat_true: ∀n,m:nat.n = m → eqbnat n m = true.
+// qed.
\ No newline at end of file
--- /dev/null
+include "basics/core_notation.ma".
+
+universe constraint Type[0] < Type[1].
+universe constraint Type[1] < Type[2].
+universe constraint Type[2] < Type[3].
+universe constraint Type[3] < Type[4].
+universe constraint Type[4] < Type[5].
--- /dev/null
+include "basics/logic.ma".
+
+(********** relations **********)
+definition relation : Type[0] → Type[0]
+≝ λA.A→A→Prop.
+
+definition reflexive: ∀A.∀R :relation A.Prop
+≝ λA.λR.∀x:A.R x x.
+
+definition symmetric: ∀A.∀R: relation A.Prop
+≝ λA.λR.∀x,y:A.R x y → R y x.
+
+definition transitive: ∀A.∀R:relation A.Prop
+≝ λA.λR.∀x,y,z:A.R x y → R y z → R x z.
+
+definition irreflexive: ∀A.∀R:relation A.Prop
+≝ λA.λR.∀x:A.¬(R x x).
+
+definition cotransitive: ∀A.∀R:relation A.Prop
+≝ λA.λR.∀x,y:A.R x y → ∀z:A. R x z ∨ R z y.
+
+definition tight_apart: ∀A.∀eq,ap:relation A.Prop
+≝ λA.λeq,ap.∀x,y:A. (¬(ap x y) → eq x y) ∧
+(eq x y → ¬(ap x y)).
+
+definition antisymmetric: ∀A.∀R:relation A.Prop
+≝ λA.λR.∀x,y:A. R x y → ¬(R y x).
+
+(********** functions **********)
+
+definition compose ≝
+ λA,B,C:Type[0].λf:B→C.λg:A→B.λx:A.f (g x).
+
+interpretation "function composition" 'compose f g = (compose ? ? ? f g).
+
+definition injective: ∀A,B:Type[0].∀ f:A→B.Prop
+≝ λA,B.λf.∀x,y:A.f x = f y → x=y.
+
+definition surjective: ∀A,B:Type[0].∀f:A→B.Prop
+≝λA,B.λf.∀z:B.∃x:A.z = f x.
+
+definition commutative: ∀A:Type[0].∀f:A→A→A.Prop
+≝ λA.λf.∀x,y.f x y = f y x.
+
+definition commutative2: ∀A,B:Type[0].∀f:A→A→B.Prop
+≝ λA,B.λf.∀x,y.f x y = f y x.
+
+definition associative: ∀A:Type[0].∀f:A→A→A.Prop
+≝ λA.λf.∀x,y,z.f (f x y) z = f x (f y z).
+
+(* functions and relations *)
+definition monotonic : ∀A:Type[0].∀R:A→A→Prop.
+∀f:A→A.Prop ≝
+λA.λR.λf.∀x,y:A.R x y → R (f x) (f y).
+
+(* functions and functions *)
+definition distributive: ∀A:Type[0].∀f,g:A→A→A.Prop
+≝ λA.λf,g.∀x,y,z:A. f x (g y z) = g (f x y) (f x z).
+
+definition distributive2: ∀A,B:Type[0].∀f:A→B→B.∀g:B→B→B.Prop
+≝ λA,B.λf,g.∀x:A.∀y,z:B. f x (g y z) = g (f x y) (f x z).
+
+(* extensional equality *)
+
+definition exteqR: ∀A,B:Type[0].∀R,S:A→B→Prop.Prop ≝
+λA,B.λR,S.∀a.∀b.iff (R a b) (S a b).
+
+definition exteqF: ∀A,B:Type[0].∀f,g:A→B.Prop ≝
+λA,B.λf,g.∀a.f a = g a.
+
+notation "x \eqR y" non associative with precedence 45
+for @{'eqR ? ? x y}.
+
+interpretation "functional extentional equality"
+'eqR A B R S = (exteqR A B R S).
+
+notation " f \eqF g " non associative with precedence 45
+for @{'eqF ? ? f g}.
+
+interpretation "functional extentional equality"
+'eqF A B f g = (exteqF A B f g).
+
--- /dev/null
+include "basics/logic.ma".
+
+(**** a subset of A is just an object of type A→Prop ****)
+
+definition empty_set ≝ λA:Type[0].λa:A.False.
+notation "\emptyv" non associative with precedence 90 for @{'empty_set}.
+interpretation "empty set" 'empty_set = (empty_set ?).
+
+definition singleton ≝ λA.λx,a:A.x=a.
+(* notation "{x}" non associative with precedence 90 for @{'sing_lang $x}. *)
+interpretation "singleton" 'singl x = (singleton ? x).
+
+definition union : ∀A:Type[0].∀P,Q.A → Prop ≝ λA,P,Q,a.P a ∨ Q a.
+interpretation "union" 'union a b = (union ? a b).
+
+definition intersection : ∀A:Type[0].∀P,Q.A→Prop ≝ λA,P,Q,a.P a ∧ Q a.
+interpretation "intersection" 'intersects a b = (intersection ? a b).
+
+definition complement ≝ λU:Type[0].λA:U → Prop.λw.¬ A w.
+interpretation "complement" 'not a = (complement ? a).
+
+definition substraction := λU:Type[0].λA,B:U → Prop.λw.A w ∧ ¬ B w.
+interpretation "substraction" 'minus a b = (substraction ? a b).
+
+definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a).
+interpretation "subset" 'subseteq a b = (subset ? a b).
+
+(* extensional equality *)
+definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a ↔ Q a.
+notation "A =1 B" non associative with precedence 45 for @{'eqP $A $B}.
+interpretation "extensional equality" 'eqP a b = (eqP ? a b).
+
+lemma eqP_sym: ∀U.∀A,B:U →Prop.
+ A =1 B → B =1 A.
+#U #A #B #eqAB #a @iff_sym @eqAB qed.
+
+lemma eqP_trans: ∀U.∀A,B,C:U →Prop.
+ A =1 B → B =1 C → A =1 C.
+#U #A #B #C #eqAB #eqBC #a @iff_trans // qed.
+
+lemma eqP_union_r: ∀U.∀A,B,C:U →Prop.
+ A =1 C → A ∪ B =1 C ∪ B.
+#U #A #B #C #eqAB #a @iff_or_r @eqAB qed.
+
+lemma eqP_union_l: ∀U.∀A,B,C:U →Prop.
+ B =1 C → A ∪ B =1 A ∪ C.
+#U #A #B #C #eqBC #a @iff_or_l @eqBC qed.
+
+lemma eqP_intersect_r: ∀U.∀A,B,C:U →Prop.
+ A =1 C → A ∩ B =1 C ∩ B.
+#U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
+
+lemma eqP_intersect_l: ∀U.∀A,B,C:U →Prop.
+ B =1 C → A ∩ B =1 A ∩ C.
+#U #A #B #C #eqBC #a @iff_and_l @eqBC qed.
+
+lemma eqP_substract_r: ∀U.∀A,B,C:U →Prop.
+ A =1 C → A - B =1 C - B.
+#U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
+
+lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop.
+ B =1 C → A - B =1 A - C.
+#U #A #B #C #eqBC #a @iff_and_l /2/ qed.
+
+(* set equalities *)
+lemma union_empty_r: ∀U.∀A:U→Prop.
+ A ∪ ∅ =1 A.
+#U #A #w % [* // normalize #abs @False_ind /2/ | /2/]
+qed.
+
+lemma union_comm : ∀U.∀A,B:U →Prop.
+ A ∪ B =1 B ∪ A.
+#U #A #B #a % * /2/ qed.
+
+lemma union_assoc: ∀U.∀A,B,C:U → Prop.
+ A ∪ B ∪ C =1 A ∪ (B ∪ C).
+#S #A #B #C #w % [* [* /3/ | /3/] | * [/3/ | * /3/]
+qed.
+
+lemma cap_comm : ∀U.∀A,B:U →Prop.
+ A ∩ B =1 B ∩ A.
+#U #A #B #a % * /2/ qed.
+
+lemma union_idemp: ∀U.∀A:U →Prop.
+ A ∪ A =1 A.
+#U #A #a % [* // | /2/] qed.
+
+lemma cap_idemp: ∀U.∀A:U →Prop.
+ A ∩ A =1 A.
+#U #A #a % [* // | /2/] qed.
+
+(*distributivities *)
+
+lemma distribute_intersect : ∀U.∀A,B,C:U→Prop.
+ (A ∪ B) ∩ C =1 (A ∩ C) ∪ (B ∩ C).
+#U #A #B #C #w % [* * /3/ | * * /3/]
+qed.
+
+lemma distribute_substract : ∀U.∀A,B,C:U→Prop.
+ (A ∪ B) - C =1 (A - C) ∪ (B - C).
+#U #A #B #C #w % [* * /3/ | * * /3/]
+qed.
+
+(* substraction *)
+lemma substract_def:∀U.∀A,B:U→Prop. A-B =1 A ∩ ¬B.
+#U #A #B #w normalize /2/
+qed.
\ No newline at end of file
--- /dev/null
+include "basics/logic.ma".
+
+(* void *)
+inductive void : Type[0] ≝.
+
+(* unit *)
+inductive unit : Type[0] ≝ it: unit.
+
+(* sum *)
+inductive Sum (A,B:Type[0]) : Type[0] ≝
+ inl : A → Sum A B
+| inr : B → Sum A B.
+
+interpretation "Disjoint union" 'plus A B = (Sum A B).
+
+(* option *)
+inductive option (A:Type[0]) : Type[0] ≝
+ None : option A
+ | Some : A → option A.
+
+definition option_map : ∀A,B:Type[0]. (A → B) → option A → option B ≝
+λA,B,f,o. match o with [ None ⇒ None B | Some a ⇒ Some B (f a) ].
+
+lemma option_map_none : ∀A,B,f,x.
+ option_map A B f x = None B → x = None A.
+#A #B #f * [ // | #a #E whd in E:(??%?); destruct ]
+qed.
+
+lemma option_map_some : ∀A,B,f,x,v.
+ option_map A B f x = Some B v → ∃y. x = Some ? y ∧ f y = v.
+#A #B #f *
+[ #v normalize #E destruct
+| #y #v normalize #E %{y} destruct % //
+] qed.
+
+definition option_map_def : ∀A,B:Type[0]. (A → B) → B → option A → B ≝
+λA,B,f,d,o. match o with [ None ⇒ d | Some a ⇒ f a ].
+
+lemma refute_none_by_refl : ∀A,B:Type[0]. ∀P:A → B. ∀Q:B → Type[0]. ∀x:option A. ∀H:x = None ? → False.
+ (∀v. x = Some ? v → Q (P v)) →
+ Q (match x return λy.x = y → ? with [ Some v ⇒ λ_. P v | None ⇒ λE. match H E in False with [ ] ] (refl ? x)).
+#A #B #P #Q *
+[ #H cases (H (refl ??))
+| #a #H #p normalize @p @refl
+] qed.
+
+(* dependent pair *)
+record DPair (A:Type[0]) (f:A→Type[0]) : Type[0] ≝ {
+ dpi1:> A
+ ; dpi2: f dpi1
+ }.
+
+interpretation "DPair" 'dpair x = (DPair ? x).
+
+interpretation "mk_DPair" 'mk_DPair x y = (mk_DPair ?? x y).
+
+(* sigma *)
+record Sig (A:Type[0]) (f:A→Prop) : Type[0] ≝ {
+ pi1: A
+ ; pi2: f pi1
+ }.
+
+interpretation "Sigma" 'sigma x = (Sig ? x).
+
+interpretation "mk_Sig" 'dp x y = (mk_Sig ?? x y).
+
+lemma sub_pi2 : ∀A.∀P,P':A → Prop. (∀x.P x → P' x) → ∀x:Σx:A.P x. P' (pi1 … x).
+#A #P #P' #H1 * #x #H2 @H1 @H2
+qed.
+
+(* Prod *)
+
+record Prod (A,B:Type[0]) : Type[0] ≝ {
+ fst: A
+ ; snd: B
+ }.
+
+interpretation "Pair construction" 'pair x y = (mk_Prod ? ? x y).
+
+interpretation "Product" 'product x y = (Prod x y).
+
+interpretation "pair pi1" 'pi1 = (fst ? ?).
+interpretation "pair pi2" 'pi2 = (snd ? ?).
+interpretation "pair pi1" 'pi1a x = (fst ? ? x).
+interpretation "pair pi2" 'pi2a x = (snd ? ? x).
+interpretation "pair pi1" 'pi1b x y = (fst ? ? x y).
+interpretation "pair pi2" 'pi2b x y = (snd ? ? x y).
+
+notation "π1" with precedence 10 for @{ (proj1 ??) }.
+notation "π2" with precedence 10 for @{ (proj2 ??) }.
+
+(* Yeah, I probably ought to do something more general... *)
+notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c\rangle)"
+with precedence 90 for @{ 'triple $a $b $c}.
+interpretation "Triple construction" 'triple x y z = (mk_Prod ? ? (mk_Prod ? ? x y) z).
+
+notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c, break term 19 d\rangle)"
+with precedence 90 for @{ 'quadruple $a $b $c $d}.
+interpretation "Quadruple construction" 'quadruple w x y z = (mk_Prod ? ? (mk_Prod ? ? w x) (mk_Prod ? ? y z)).
+
+
+theorem eq_pair_fst_snd: ∀A,B.∀p:A × B.
+ p = 〈 \fst p, \snd p 〉.
+#A #B #p (cases p) // qed.
+
+lemma fst_eq : ∀A,B.∀a:A.∀b:B. \fst 〈a,b〉 = a.
+// qed.
+
+lemma snd_eq : ∀A,B.∀a:A.∀b:B. \snd 〈a,b〉 = b.
+// qed.
+
+notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
+ with precedence 10
+for @{ match $t with [ mk_Prod ${ident x} ${ident y} ⇒ $s ] }.
+
+notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉 \nbsp≝ break t \nbsp 'in' \nbsp) break s)"
+ with precedence 10
+for @{ match $t with [ mk_Prod (${ident x}:$X) (${ident y}:$Y) ⇒ $s ] }.
+
+(* Also extracts an equality proof (useful when not using Russell). *)
+notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)"
+ with precedence 10
+for @{ match $t return λx.x = $t → ? with [ mk_Prod ${ident x} ${ident y} ⇒
+ λ${ident E}.$s ] (refl ? $t) }.
+
+notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉 \nbsp 'as'\nbsp ident E\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
+ with precedence 10
+for @{ match $t return λ${ident k}:$X.$eq $T $k $t → ? with [ mk_Prod (${ident x}:$U) (${ident y}:$W) ⇒
+ λ${ident E}:$e.$s ] ($refl $T $t) }.
+
+notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)"
+ with precedence 10
+for @{ match $t return λx.x = $t → ? with [ mk_Prod ${fresh xy} ${ident z} ⇒
+ match ${fresh xy} return λx. ? = $t → ? with [ mk_Prod ${ident x} ${ident y} ⇒
+ λ${ident E}.$s ] ] (refl ? $t) }.
+
+notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y,ident z〉 \nbsp'as'\nbsp ident E\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
+ with precedence 10
+for @{ match $t return λ${ident x}.$eq $T $x $t → $U with [ mk_Prod (${fresh xy}:$V) (${ident z}:$Z) ⇒
+ match ${fresh xy} return λ${ident y}. $eq $R $r $t → ? with [ mk_Prod (${ident x}:$L) (${ident y}:$I) ⇒
+ λ${ident E}:$J.$s ] ] ($refl $A $t) }.
+
+notation > "hvbox('let' 〈ident w,ident x,ident y,ident z〉 ≝ t 'in' s)"
+ with precedence 10
+for @{ match $t with [ mk_Prod ${fresh wx} ${fresh yz} ⇒ match ${fresh wx} with [ mk_Prod ${ident w} ${ident x} ⇒ match ${fresh yz} with [ mk_Prod ${ident y} ${ident z} ⇒ $s ] ] ] }.
+
+notation > "hvbox('let' 〈ident x,ident y,ident z〉 ≝ t 'in' s)"
+ with precedence 10
+for @{ match $t with [ mk_Prod ${fresh xy} ${ident z} ⇒ match ${fresh xy} with [ mk_Prod ${ident x} ${ident y} ⇒ $s ] ] }.
+
+(* This appears to upset automation (previously provable results require greater
+ depth or just don't work), so use example rather than lemma to prevent it
+ being indexed. *)
+example contract_pair : ∀A,B.∀e:A×B. (let 〈a,b〉 ≝ e in 〈a,b〉) = e.
+#A #B * // qed.
+
+lemma extract_pair : ∀A,B,C,D. ∀u:A×B. ∀Q:A → B → C×D. ∀x,y.
+((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) →
+∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉.
+#A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 qed.
+
+lemma breakup_pair : ∀A,B,C:Type[0].∀x. ∀R:C → Prop. ∀P:A → B → C.
+ R (P (\fst x) (\snd x)) → R (let 〈a,b〉 ≝ x in P a b).
+#A #B #C *; normalize /2/
+qed.
+
+lemma pair_elim:
+ ∀A,B,C: Type[0].
+ ∀T: A → B → C.
+ ∀p.
+ ∀P: A×B → C → Prop.
+ (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt)) →
+ P p (let 〈lft, rgt〉 ≝ p in T lft rgt).
+ #A #B #C #T * /2/
+qed.
+
+lemma pair_elim2:
+ ∀A,B,C,C': Type[0].
+ ∀T: A → B → C.
+ ∀T': A → B → C'.
+ ∀p.
+ ∀P: A×B → C → C' → Prop.
+ (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt) (T' lft rgt)) →
+ P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt).
+ #A #B #C #C' #T #T' * /2/
+qed.
+
+(* Useful for avoiding destruct's full normalization. *)
+lemma pair_eq1: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → a1 = a2.
+#A #B #a1 #a2 #b1 #b2 #H destruct //
+qed.
+
+lemma pair_eq2: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → b1 = b2.
+#A #B #a1 #a2 #b1 #b2 #H destruct //
+qed.
+
+lemma pair_destruct_1:
+ ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → a = \fst c.
+ #A #B #a #b *; /2/
+qed.
+
+lemma pair_destruct_2:
+ ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → b = \snd c.
+ #A #B #a #b *; /2/
+qed.
+
+lemma coerc_pair_sigma:
+ ∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x).
+#A #B #P * #a #b #p % [@a | /2/]
+qed.
+coercion coerc_pair_sigma:∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x)
+≝ coerc_pair_sigma on p: (? × ?) to (? × (Sig ??)).
--- /dev/null
+include "basics/list.ma".
+include "basics/sets.ma".
+include "basics/deqsets.ma".
+
+definition word ≝ λS:DeqSet.list S.
+
+notation "ϵ" non associative with precedence 90 for @{ 'epsilon }.
+interpretation "epsilon" 'epsilon = (nil ?).
+
+(* concatenation *)
+definition cat : ∀S,l1,l2,w.Prop ≝
+ λS.λl1,l2.λw:word S.∃w1,w2.w1 @ w2 = w ∧ l1 w1 ∧ l2 w2.
+notation "a · b" non associative with precedence 60 for @{ 'middot $a $b}.
+interpretation "cat lang" 'middot a b = (cat ? a b).
+
+let rec flatten (S : DeqSet) (l : list (word S)) on l : word S ≝
+match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
+
+let rec conjunct (S : DeqSet) (l : list (word S)) (r : word S → Prop) on l: Prop ≝
+match l with [ nil ⇒ True | cons w tl ⇒ r w ∧ conjunct ? tl r ].
+
+(* kleene's star *)
+definition star ≝ λS.λl.λw:word S.∃lw.flatten ? lw = w ∧ conjunct ? lw l.
+notation "a ^ *" non associative with precedence 90 for @{ 'star $a}.
+interpretation "star lang" 'star l = (star ? l).
+
+lemma cat_ext_l: ∀S.∀A,B,C:word S →Prop.
+ A =1 C → A · B =1 C · B.
+#S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2
+cases (H w1) /6/
+qed.
+
+lemma cat_ext_r: ∀S.∀A,B,C:word S →Prop.
+ B =1 C → A · B =1 A · C.
+#S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2
+cases (H w2) /6/
+qed.
+
+lemma cat_empty_l: ∀S.∀A:word S→Prop. ∅ · A =1 ∅.
+#S #A #w % [|*] * #w1 * #w2 * * #_ *
+qed.
+
+lemma distr_cat_r: ∀S.∀A,B,C:word S →Prop.
+ (A ∪ B) · C =1 A · C ∪ B · C.
+#S #A #B #C #w %
+ [* #w1 * #w2 * * #eqw * /6/ |* * #w1 * #w2 * * /6/]
+qed.
+
+(* derivative *)
+
+definition deriv ≝ λS.λA:word S → Prop.λa,w. A (a::w).
+
+lemma deriv_middot: ∀S,A,B,a. ¬ A ϵ →
+ deriv S (A·B) a =1 (deriv S A a) · B.
+#S #A #B #a #noteps #w normalize %
+ [* #w1 cases w1
+ [* #w2 * * #_ #Aeps @False_ind /2/
+ |#b #w2 * #w3 * * whd in ⊢ ((??%?)→?); #H destruct
+ #H #H1 @(ex_intro … w2) @(ex_intro … w3) % // % //
+ ]
+ |* #w1 * #w2 * * #H #H1 #H2 @(ex_intro … (a::w1))
+ @(ex_intro … w2) % // % normalize //
+ ]
+qed.
+
+(* star properties *)
+lemma espilon_in_star: ∀S.∀A:word S → Prop.
+ A^* ϵ.
+#S #A @(ex_intro … [ ]) normalize /2/
+qed.
+
+lemma cat_to_star:∀S.∀A:word S → Prop.
+ ∀w1,w2. A w1 → A^* w2 → A^* (w1@w2).
+#S #A #w1 #w2 #Aw * #l * #H #H1 @(ex_intro … (w1::l))
+% normalize /2/
+qed.
+
+lemma fix_star: ∀S.∀A:word S → Prop.
+ A^* =1 A · A^* ∪ {ϵ}.
+#S #A #w %
+ [* #l generalize in match w; -w cases l [normalize #w * /2/]
+ #w1 #tl #w * whd in ⊢ ((??%?)→?); #eqw whd in ⊢ (%→?); *
+ #w1A #cw1 %1 @(ex_intro … w1) @(ex_intro … (flatten S tl))
+ % /2/ whd @(ex_intro … tl) /2/
+ |* [2: whd in ⊢ (%→?); #eqw <eqw //]
+ * #w1 * #w2 * * #eqw <eqw @cat_to_star
+ ]
+qed.
+
+lemma star_fix_eps : ∀S.∀A:word S → Prop.
+ A^* =1 (A - {ϵ}) · A^* ∪ {ϵ}.
+#S #A #w %
+ [* #l elim l
+ [* whd in ⊢ ((??%?)→?); #eqw #_ %2 <eqw //
+ |* [#tl #Hind * #H * #_ #H2 @Hind % [@H | //]
+ |#a #w1 #tl #Hind * whd in ⊢ ((??%?)→?); #H1 * #H2 #H3 %1
+ @(ex_intro … (a::w1)) @(ex_intro … (flatten S tl)) %
+ [% [@H1 | normalize % /2/] |whd @(ex_intro … tl) /2/]
+ ]
+ ]
+ |* [* #w1 * #w2 * * #eqw * #H1 #_ <eqw @cat_to_star //
+ | whd in ⊢ (%→?); #H <H //
+ ]
+ ]
+qed.
+
+lemma star_epsilon: ∀S:DeqSet.∀A:word S → Prop.
+ A^* ∪ {ϵ} =1 A^*.
+#S #A #w % /2/ * //
+qed.
+
+lemma epsilon_cat_r: ∀S.∀A:word S →Prop.
+ A · {ϵ} =1 A.
+#S #A #w %
+ [* #w1 * #w2 * * #eqw #inw1 normalize #eqw2 <eqw //
+ |#inA @(ex_intro … w) @(ex_intro … [ ]) /3/
+ ]
+qed.
+
+lemma epsilon_cat_l: ∀S.∀A:word S →Prop.
+ {ϵ} · A =1 A.
+#S #A #w %
+ [* #w1 * #w2 * * #eqw normalize #eqw2 <eqw <eqw2 //
+ |#inA @(ex_intro … ϵ) @(ex_intro … w) /3/
+ ]
+qed.
+
+lemma distr_cat_r_eps: ∀S.∀A,C:word S →Prop.
+ (A ∪ {ϵ}) · C =1 A · C ∪ C.
+#S #A #C @eqP_trans [|@distr_cat_r |@eqP_union_l @epsilon_cat_l]
+qed.
+
--- /dev/null
+include "re.ma".
+include "basics/listb.ma".
+
+let rec move (S: DeqSet) (x:S) (E: pitem S) on E : pre S ≝
+ match E with
+ [ pz ⇒ 〈 `∅, false 〉
+ | pe ⇒ 〈 ϵ, false 〉
+ | ps y ⇒ 〈 `y, false 〉
+ | pp y ⇒ 〈 `y, x == y 〉
+ | po e1 e2 ⇒ (move ? x e1) ⊕ (move ? x e2)
+ | pc e1 e2 ⇒ (move ? x e1) ⊙ (move ? x e2)
+ | pk e ⇒ (move ? x e)^⊛ ].
+
+lemma move_plus: ∀S:DeqSet.∀x:S.∀i1,i2:pitem S.
+ move S x (i1 + i2) = (move ? x i1) ⊕ (move ? x i2).
+// qed.
+
+lemma move_cat: ∀S:DeqSet.∀x:S.∀i1,i2:pitem S.
+ move S x (i1 · i2) = (move ? x i1) ⊙ (move ? x i2).
+// qed.
+
+lemma move_star: ∀S:DeqSet.∀x:S.∀i:pitem S.
+ move S x i^* = (move ? x i)^⊛.
+// qed.
+
+definition pmove ≝ λS:DeqSet.λx:S.λe:pre S. move ? x (\fst e).
+
+lemma pmove_def : ∀S:DeqSet.∀x:S.∀i:pitem S.∀b.
+ pmove ? x 〈i,b〉 = move ? x i.
+// qed.
+
+lemma eq_to_eq_hd: ∀A.∀l1,l2:list A.∀a,b.
+ a::l1 = b::l2 → a = b.
+#A #l1 #l2 #a #b #H destruct //
+qed.
+
+lemma same_kernel: ∀S:DeqSet.∀a:S.∀i:pitem S.
+ |\fst (move ? a i)| = |i|.
+#S #a #i elim i //
+ [#i1 #i2 #H1 #H2 >move_cat >erase_odot //
+ |#i1 #i2 #H1 #H2 >move_plus whd in ⊢ (??%%); //
+ ]
+qed.
+
+theorem move_ok:
+ ∀S:DeqSet.∀a:S.∀i:pitem S.∀w: word S.
+ \sem{move ? a i} w ↔ \sem{i} (a::w).
+#S #a #i elim i
+ [normalize /2/
+ |normalize /2/
+ |normalize /2/
+ |normalize #x #w cases (true_or_false (a==x)) #H >H normalize
+ [>(\P H) % [* // #bot @False_ind //| #H1 destruct /2/]
+ |% [@False_ind |#H1 cases (\Pf H) #H2 @H2 destruct //]
+ ]
+ |#i1 #i2 #HI1 #HI2 #w >move_cat
+ @iff_trans[|@sem_odot] >same_kernel >sem_cat_w
+ @iff_trans[||@(iff_or_l … (HI2 w))] @iff_or_r
+ @iff_trans[||@iff_sym @deriv_middot //]
+ @cat_ext_l @HI1
+ |#i1 #i2 #HI1 #HI2 #w >(sem_plus S i1 i2) >move_plus >sem_plus_w
+ @iff_trans[|@sem_oplus]
+ @iff_trans[|@iff_or_l [|@HI2]| @iff_or_r //]
+ |#i1 #HI1 #w >move_star
+ @iff_trans[|@sem_ostar] >same_kernel >sem_star_w
+ @iff_trans[||@iff_sym @deriv_middot //]
+ @cat_ext_l @HI1
+ ]
+qed.
+
+notation > "x ↦* E" non associative with precedence 60 for @{moves ? $x $E}.
+let rec moves (S : DeqSet) w e on w : pre S ≝
+ match w with
+ [ nil ⇒ e
+ | cons x w' ⇒ w' ↦* (move S x (\fst e))].
+
+lemma moves_empty: ∀S:DeqSet.∀e:pre S.
+ moves ? [ ] e = e.
+// qed.
+
+lemma moves_cons: ∀S:DeqSet.∀a:S.∀w.∀e:pre S.
+ moves ? (a::w) e = moves ? w (move S a (\fst e)).
+// qed.
+
+lemma moves_left : ∀S,a,w,e.
+ moves S (w@[a]) e = move S a (\fst (moves S w e)).
+#S #a #w elim w // #x #tl #Hind #e >moves_cons >moves_cons //
+qed.
+
+lemma not_epsilon_sem: ∀S:DeqSet.∀a:S.∀w: word S. ∀e:pre S.
+ iff ((a::w) ∈ e) ((a::w) ∈ \fst e).
+#S #a #w * #i #b cases b normalize
+ [% /2/ * // #H destruct |% normalize /2/]
+qed.
+
+lemma same_kernel_moves: ∀S:DeqSet.∀w.∀e:pre S.
+ |\fst (moves ? w e)| = |\fst e|.
+#S #w elim w //
+qed.
+
+theorem decidable_sem: ∀S:DeqSet.∀w: word S. ∀e:pre S.
+ (\snd (moves ? w e) = true) ↔ \sem{e} w.
+#S #w elim w
+ [* #i #b >moves_empty cases b % /2/
+ |#a #w1 #Hind #e >moves_cons
+ @iff_trans [||@iff_sym @not_epsilon_sem]
+ @iff_trans [||@move_ok] @Hind
+ ]
+qed.
+
+(************************ pit state ***************************)
+definition pit_pre ≝ λS.λi.〈blank S (|i|), false〉.
+
+let rec occur (S: DeqSet) (i: re S) on i ≝
+ match i with
+ [ z ⇒ [ ]
+ | e ⇒ [ ]
+ | s y ⇒ [y]
+ | o e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2)
+ | c e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2)
+ | k e ⇒ occur S e].
+
+lemma not_occur_to_pit: ∀S,a.∀i:pitem S. memb S a (occur S (|i|)) ≠ true →
+ move S a i = pit_pre S i.
+#S #a #i elim i //
+ [#x normalize cases (a==x) normalize // #H @False_ind /2/
+ |#i1 #i2 #Hind1 #Hind2 #H >move_cat
+ >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //]
+ >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] //
+ |#i1 #i2 #Hind1 #Hind2 #H >move_plus
+ >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //]
+ >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] //
+ |#i #Hind #H >move_star >Hind //
+ ]
+qed.
+
+lemma move_pit: ∀S,a,i. move S a (\fst (pit_pre S i)) = pit_pre S i.
+#S #a #i elim i //
+ [#i1 #i2 #Hind1 #Hind2 >move_cat >Hind1 >Hind2 //
+ |#i1 #i2 #Hind1 #Hind2 >move_plus >Hind1 >Hind2 //
+ |#i #Hind >move_star >Hind //
+ ]
+qed.
+
+lemma moves_pit: ∀S,w,i. moves S w (pit_pre S i) = pit_pre S i.
+#S #w #i elim w //
+qed.
+
+lemma to_pit: ∀S,w,e. ¬ sublist S w (occur S (|\fst e|)) →
+ moves S w e = pit_pre S (\fst e).
+#S #w elim w
+ [#e * #H @False_ind @H normalize #a #abs @False_ind /2/
+ |#a #tl #Hind #e #H cases (true_or_false (memb S a (occur S (|\fst e|))))
+ [#Htrue >moves_cons whd in ⊢ (???%); <(same_kernel … a)
+ @Hind >same_kernel @(not_to_not … H) #H1 #b #memb cases (orb_true_l … memb)
+ [#H2 >(\P H2) // |#H2 @H1 //]
+ |#Hfalse >moves_cons >not_occur_to_pit // >Hfalse /2/
+ ]
+ ]
+qed.
+
+(* bisimulation *)
+definition cofinal ≝ λS.λp:(pre S)×(pre S).
+ \snd (\fst p) = \snd (\snd p).
+
+theorem equiv_sem: ∀S:DeqSet.∀e1,e2:pre S.
+ \sem{e1} =1 \sem{e2} ↔ ∀w.cofinal ? 〈moves ? w e1,moves ? w e2〉.
+#S #e1 #e2 %
+[#same_sem #w
+ cut (∀b1,b2. iff (b1 = true) (b2 = true) → (b1 = b2))
+ [* * // * #H1 #H2 [@sym_eq @H1 //| @H2 //]]
+ #Hcut @Hcut @iff_trans [|@decidable_sem]
+ @iff_trans [|@same_sem] @iff_sym @decidable_sem
+|#H #w1 @iff_trans [||@decidable_sem] <H @iff_sym @decidable_sem]
+qed.
+
+definition occ ≝ λS.λe1,e2:pre S.
+ unique_append ? (occur S (|\fst e1|)) (occur S (|\fst e2|)).
+
+lemma occ_enough: ∀S.∀e1,e2:pre S.
+(∀w.(sublist S w (occ S e1 e2))→ cofinal ? 〈moves ? w e1,moves ? w e2〉)
+ →∀w.cofinal ? 〈moves ? w e1,moves ? w e2〉.
+#S #e1 #e2 #H #w
+cases (decidable_sublist S w (occ S e1 e2)) [@H] -H #H
+ >to_pit [2: @(not_to_not … H) #H1 #a #memba @sublist_unique_append_l1 @H1 //]
+ >to_pit [2: @(not_to_not … H) #H1 #a #memba @sublist_unique_append_l2 @H1 //]
+ //
+qed.
+
+lemma equiv_sem_occ: ∀S.∀e1,e2:pre S.
+(∀w.(sublist S w (occ S e1 e2))→ cofinal ? 〈moves ? w e1,moves ? w e2〉)
+→ \sem{e1}=1\sem{e2}.
+#S #e1 #e2 #H @(proj2 … (equiv_sem …)) @occ_enough #w @H
+qed.
+
+definition sons ≝ λS:DeqSet.λl:list S.λp:(pre S)×(pre S).
+ map ?? (λa.〈move S a (\fst (\fst p)),move S a (\fst (\snd p))〉) l.
+
+lemma memb_sons: ∀S,l.∀p,q:(pre S)×(pre S). memb ? p (sons ? l q) = true →
+ ∃a.(move ? a (\fst (\fst q)) = \fst p ∧
+ move ? a (\fst (\snd q)) = \snd p).
+#S #l elim l [#p #q normalize in ⊢ (%→?); #abs @False_ind /2/]
+#a #tl #Hind #p #q #H cases (orb_true_l … H) -H
+ [#H @(ex_intro … a) >(\P H) /2/ |#H @Hind @H]
+qed.
+
+definition is_bisim ≝ λS:DeqSet.λl:list ?.λalpha:list S.
+ ∀p:(pre S)×(pre S). memb ? p l = true → cofinal ? p ∧ (sublist ? (sons ? alpha p) l).
+
+lemma bisim_to_sem: ∀S:DeqSet.∀l:list ?.∀e1,e2: pre S.
+ is_bisim S l (occ S e1 e2) → memb ? 〈e1,e2〉 l = true → \sem{e1}=1\sem{e2}.
+#S #l #e1 #e2 #Hbisim #Hmemb @equiv_sem_occ
+#w #Hsub @(proj1 … (Hbisim 〈moves S w e1,moves S w e2〉 ?))
+lapply Hsub @(list_elim_left … w) [//]
+#a #w1 #Hind #Hsub >moves_left >moves_left @(proj2 …(Hbisim …(Hind ?)))
+ [#x #Hx @Hsub @memb_append_l1 //
+ |cut (memb S a (occ S e1 e2) = true) [@Hsub @memb_append_l2 //] #occa
+ @(memb_map … occa)
+ ]
+qed.
+
+(* the algorithm *)
+let rec bisim S l n (frontier,visited: list ?) on n ≝
+ match n with
+ [ O ⇒ 〈false,visited〉 (* assert false *)
+ | S m ⇒
+ match frontier with
+ [ nil ⇒ 〈true,visited〉
+ | cons hd tl ⇒
+ if beqb (\snd (\fst hd)) (\snd (\snd hd)) then
+ bisim S l m (unique_append ? (filter ? (λx.notb (memb ? x (hd::visited)))
+ (sons S l hd)) tl) (hd::visited)
+ else 〈false,visited〉
+ ]
+ ].
+
+lemma unfold_bisim: ∀S,l,n.∀frontier,visited: list ?.
+ bisim S l n frontier visited =
+ match n with
+ [ O ⇒ 〈false,visited〉 (* assert false *)
+ | S m ⇒
+ match frontier with
+ [ nil ⇒ 〈true,visited〉
+ | cons hd tl ⇒
+ if beqb (\snd (\fst hd)) (\snd (\snd hd)) then
+ bisim S l m (unique_append ? (filter ? (λx.notb(memb ? x (hd::visited)))
+ (sons S l hd)) tl) (hd::visited)
+ else 〈false,visited〉
+ ]
+ ].
+#S #l #n cases n // qed.
+
+lemma bisim_never: ∀S,l.∀frontier,visited: list ?.
+ bisim S l O frontier visited = 〈false,visited〉.
+#frontier #visited >unfold_bisim //
+qed.
+
+lemma bisim_end: ∀Sig,l,m.∀visited: list ?.
+ bisim Sig l (S m) [] visited = 〈true,visited〉.
+#n #visisted >unfold_bisim //
+qed.
+
+lemma bisim_step_true: ∀Sig,l,m.∀p.∀frontier,visited: list ?.
+beqb (\snd (\fst p)) (\snd (\snd p)) = true →
+ bisim Sig l (S m) (p::frontier) visited =
+ bisim Sig l m (unique_append ? (filter ? (λx.notb(memb ? x (p::visited)))
+ (sons Sig l p)) frontier) (p::visited).
+#Sig #l #m #p #frontier #visited #test >unfold_bisim normalize nodelta >test //
+qed.
+
+lemma bisim_step_false: ∀Sig,l,m.∀p.∀frontier,visited: list ?.
+beqb (\snd (\fst p)) (\snd (\snd p)) = false →
+ bisim Sig l (S m) (p::frontier) visited = 〈false,visited〉.
+#Sig #l #m #p #frontier #visited #test >unfold_bisim normalize nodelta >test //
+qed.
+
+lemma notb_eq_true_l: ∀b. notb b = true → b = false.
+#b cases b normalize //
+qed.
+
+let rec pitem_enum S (i:re S) on i ≝
+ match i with
+ [ z ⇒ [pz S]
+ | e ⇒ [pe S]
+ | s y ⇒ [ps S y; pp S y]
+ | o i1 i2 ⇒ compose ??? (po S) (pitem_enum S i1) (pitem_enum S i2)
+ | c i1 i2 ⇒ compose ??? (pc S) (pitem_enum S i1) (pitem_enum S i2)
+ | k i ⇒ map ?? (pk S) (pitem_enum S i)
+ ].
+
+lemma pitem_enum_complete : ∀S.∀i:pitem S.
+ memb (DeqItem S) i (pitem_enum S (|i|)) = true.
+#S #i elim i
+ [1,2://
+ |3,4:#c normalize >(\b (refl … c)) //
+ |5,6:#i1 #i2 #Hind1 #Hind2 @(memb_compose (DeqItem S) (DeqItem S)) //
+ |#i #Hind @(memb_map (DeqItem S)) //
+ ]
+qed.
+
+definition pre_enum ≝ λS.λi:re S.
+ compose ??? (λi,b.〈i,b〉) (pitem_enum S i) [true;false].
+
+lemma pre_enum_complete : ∀S.∀e:pre S.
+ memb ? e (pre_enum S (|\fst e|)) = true.
+#S * #i #b @(memb_compose (DeqItem S) DeqBool ? (λi,b.〈i,b〉))
+// cases b normalize //
+qed.
+
+definition space_enum ≝ λS.λi1,i2:re S.
+ compose ??? (λe1,e2.〈e1,e2〉) (pre_enum S i1) (pre_enum S i2).
+
+lemma space_enum_complete : ∀S.∀e1,e2: pre S.
+ memb ? 〈e1,e2〉 (space_enum S (|\fst e1|) (|\fst e2|)) = true.
+#S #e1 #e2 @(memb_compose … (λi,b.〈i,b〉))
+// qed.
+
+definition all_reachable ≝ λS.λe1,e2:pre S.λl: list ?.
+uniqueb ? l = true ∧
+ ∀p. memb ? p l = true →
+ ∃w.(moves S w e1 = \fst p) ∧ (moves S w e2 = \snd p).
+
+definition disjoint ≝ λS:DeqSet.λl1,l2.
+ ∀p:S. memb S p l1 = true → memb S p l2 = false.
+
+lemma bisim_correct: ∀S.∀e1,e2:pre S.\sem{e1}=1\sem{e2} →
+ ∀l,n.∀frontier,visited:list ((pre S)×(pre S)).
+ |space_enum S (|\fst e1|) (|\fst e2|)| < n + |visited|→
+ all_reachable S e1 e2 visited →
+ all_reachable S e1 e2 frontier →
+ disjoint ? frontier visited →
+ \fst (bisim S l n frontier visited) = true.
+#Sig #e1 #e2 #same #l #n elim n
+ [#frontier #visited #abs * #unique #H @False_ind @(absurd … abs)
+ @le_to_not_lt @sublist_length // * #e11 #e21 #membp
+ cut ((|\fst e11| = |\fst e1|) ∧ (|\fst e21| = |\fst e2|))
+ [|* #H1 #H2 <H1 <H2 @space_enum_complete]
+ cases (H … membp) #w * #we1 #we2 <we1 <we2 % >same_kernel_moves //
+ |#m #HI * [#visited #vinv #finv >bisim_end //]
+ #p #front_tl #visited #Hn * #u_visited #r_visited * #u_frontier #r_frontier
+ #disjoint
+ cut (∃w.(moves ? w e1 = \fst p) ∧ (moves ? w e2 = \snd p))
+ [@(r_frontier … (memb_hd … ))] #rp
+ cut (beqb (\snd (\fst p)) (\snd (\snd p)) = true)
+ [cases rp #w * #fstp #sndp <fstp <sndp @(\b ?)
+ @(proj1 … (equiv_sem … )) @same] #ptest
+ >(bisim_step_true … ptest) @HI -HI
+ [<plus_n_Sm //
+ |% [whd in ⊢ (??%?); >(disjoint … (memb_hd …)) whd in ⊢ (??%?); //
+ |#p1 #H (cases (orb_true_l … H)) [#eqp >(\P eqp) // |@r_visited]
+ ]
+ |whd % [@unique_append_unique @(andb_true_r … u_frontier)]
+ @unique_append_elim #q #H
+ [cases (memb_sons … (memb_filter_memb … H)) -H
+ #a * #m1 #m2 cases rp #w1 * #mw1 #mw2 @(ex_intro … (w1@[a]))
+ >moves_left >moves_left >mw1 >mw2 >m1 >m2 % //
+ |@r_frontier @memb_cons //
+ ]
+ |@unique_append_elim #q #H
+ [@injective_notb @(filter_true … H)
+ |cut ((q==p) = false)
+ [|#Hpq whd in ⊢ (??%?); >Hpq @disjoint @memb_cons //]
+ cases (andb_true … u_frontier) #notp #_ @(\bf ?)
+ @(not_to_not … not_eq_true_false) #eqqp <notp <eqqp >H //
+ ]
+ ]
+ ]
+qed.
+
+definition all_true ≝ λS.λl.∀p:(pre S) × (pre S). memb ? p l = true →
+ (beqb (\snd (\fst p)) (\snd (\snd p)) = true).
+
+definition sub_sons ≝ λS,l,l1,l2.∀x:(pre S) × (pre S).
+memb ? x l1 = true → sublist ? (sons ? l x) l2.
+
+lemma bisim_complete:
+ ∀S,l,n.∀frontier,visited,visited_res:list ?.
+ all_true S visited →
+ sub_sons S l visited (frontier@visited) →
+ bisim S l n frontier visited = 〈true,visited_res〉 →
+ is_bisim S visited_res l ∧ sublist ? (frontier@visited) visited_res.
+#S #l #n elim n
+ [#fron #vis #vis_res #_ #_ >bisim_never #H destruct
+ |#m #Hind *
+ [(* case empty frontier *)
+ -Hind #vis #vis_res #allv #H normalize in ⊢ (%→?);
+ #H1 destruct % #p
+ [#membp % [@(\P ?) @allv //| @H //]|#H1 @H1]
+ |#hd cases (true_or_false (beqb (\snd (\fst hd)) (\snd (\snd hd))))
+ [|(* case head of the frontier is non ok (absurd) *)
+ #H #tl #vis #vis_res #allv >(bisim_step_false … H) #_ #H1 destruct]
+ (* frontier = hd:: tl and hd is ok *)
+ #H #tl #visited #visited_res #allv >(bisim_step_true … H)
+ (* new_visited = hd::visited are all ok *)
+ cut (all_true S (hd::visited))
+ [#p #H1 cases (orb_true_l … H1) [#eqp >(\P eqp) @H |@allv]]
+ (* we now exploit the induction hypothesis *)
+ #allh #subH #bisim cases (Hind … allh … bisim) -bisim -Hind
+ [#H1 #H2 % // #p #membp @H2 -H2 cases (memb_append … membp) -membp #membp
+ [cases (orb_true_l … membp) -membp #membp
+ [@memb_append_l2 >(\P membp) @memb_hd
+ |@memb_append_l1 @sublist_unique_append_l2 //
+ ]
+ |@memb_append_l2 @memb_cons //
+ ]
+ |(* the only thing left to prove is the sub_sons invariant *)
+ #x #membx cases (orb_true_l … membx)
+ [(* case x = hd *)
+ #eqhdx <(\P eqhdx) #xa #membxa
+ (* xa is a son of x; we must distinguish the case xa
+ was already visited form the case xa is new *)
+ cases (true_or_false … (memb ? xa (x::visited)))
+ [(* xa visited - trivial *) #membxa @memb_append_l2 //
+ |(* xa new *) #membxa @memb_append_l1 @sublist_unique_append_l1 @memb_filter_l
+ [>membxa //|//]
+ ]
+ |(* case x in visited *)
+ #H1 #xa #membxa cases (memb_append … (subH x … H1 … membxa))
+ [#H2 (cases (orb_true_l … H2))
+ [#H3 @memb_append_l2 <(\P H3) @memb_hd
+ |#H3 @memb_append_l1 @sublist_unique_append_l2 @H3
+ ]
+ |#H2 @memb_append_l2 @memb_cons @H2
+ ]
+ ]
+ ]
+ ]
+qed.
+
+definition equiv ≝ λSig.λre1,re2:re Sig.
+ let e1 ≝ •(blank ? re1) in
+ let e2 ≝ •(blank ? re2) in
+ let n ≝ S (length ? (space_enum Sig (|\fst e1|) (|\fst e2|))) in
+ let sig ≝ (occ Sig e1 e2) in
+ (bisim ? sig n [〈e1,e2〉] []).
+
+theorem euqiv_sem : ∀Sig.∀e1,e2:re Sig.
+ \fst (equiv ? e1 e2) = true ↔ \sem{e1} =1 \sem{e2}.
+#Sig #re1 #re2 %
+ [#H @eqP_trans [|@eqP_sym @re_embedding] @eqP_trans [||@re_embedding]
+ cut (equiv ? re1 re2 = 〈true,\snd (equiv ? re1 re2)〉)
+ [<H //] #Hcut
+ cases (bisim_complete … Hcut)
+ [2,3: #p whd in ⊢ ((??%?)→?); #abs @False_ind /2/]
+ #Hbisim #Hsub @(bisim_to_sem … Hbisim)
+ @Hsub @memb_hd
+ |#H @(bisim_correct ? (•(blank ? re1)) (•(blank ? re2)))
+ [@eqP_trans [|@re_embedding] @eqP_trans [|@H] @eqP_sym @re_embedding
+ |//
+ |% // #p whd in ⊢ ((??%?)→?); #abs @False_ind /2/
+ |% // #p #H >(memb_single … H) @(ex_intro … ϵ) /2/
+ |#p #_ normalize //
+ ]
+ ]
+qed.
+
+lemma eqbnat_true : ∀n,m. eqbnat n m = true ↔ n = m.
+#n #m % [@eqbnat_true_to_eq | @eq_to_eqbnat_true]
+qed.
+
+definition DeqNat ≝ mk_DeqSet nat eqbnat eqbnat_true.
+
+definition a ≝ s DeqNat O.
+definition b ≝ s DeqNat (S O).
+definition c ≝ s DeqNat (S (S O)).
+
+definition exp1 ≝ ((a·b)^*·a).
+definition exp2 ≝ a·(b·a)^*.
+definition exp4 ≝ (b·a)^*.
+
+definition exp6 ≝ a·(a ·a ·b^* + b^* ).
+definition exp7 ≝ a · a^* · b^*.
+
+definition exp8 ≝ a·a·a·a·a·a·a·a·(a^* ).
+definition exp9 ≝ (a·a·a + a·a·a·a·a)^*.
+
+example ex1 : \fst (equiv ? (exp8+exp9) exp9) = true.
+normalize // qed.
+
+
+
+
+
+
+
--- /dev/null
+include "lang.ma".
+
+inductive re (S: DeqSet) : Type[0] ≝
+ z: re S
+ | e: re S
+ | s: S → re S
+ | c: re S → re S → re S
+ | o: re S → re S → re S
+ | k: re S → re S.
+
+interpretation "re epsilon" 'epsilon = (e ?).
+interpretation "re or" 'plus a b = (o ? a b).
+interpretation "re cat" 'middot a b = (c ? a b).
+interpretation "re star" 'star a = (k ? a).
+
+notation < "a" non associative with precedence 90 for @{ 'ps $a}.
+notation > "` term 90 a" non associative with precedence 90 for @{ 'ps $a}.
+interpretation "atom" 'ps a = (s ? a).
+
+notation "`∅" non associative with precedence 90 for @{ 'empty }.
+interpretation "empty" 'empty = (z ?).
+
+let rec in_l (S : DeqSet) (r : re S) on r : word S → Prop ≝
+match r with
+[ z ⇒ ∅
+| e ⇒ {ϵ}
+| s x ⇒ {[x]}
+| c r1 r2 ⇒ (in_l ? r1) · (in_l ? r2)
+| o r1 r2 ⇒ (in_l ? r1) ∪ (in_l ? r2)
+| k r1 ⇒ (in_l ? r1) ^*].
+
+notation "\sem{term 19 E}" non associative with precedence 75 for @{'in_l $E}.
+interpretation "in_l" 'in_l E = (in_l ? E).
+interpretation "in_l mem" 'mem w l = (in_l ? l w).
+
+lemma rsem_star : ∀S.∀r: re S. \sem{r^*} = \sem{r}^*.
+// qed.
+
+
+(* pointed items *)
+inductive pitem (S: DeqSet) : Type[0] ≝
+ pz: pitem S
+ | pe: pitem S
+ | ps: S → pitem S
+ | pp: S → pitem S
+ | pc: pitem S → pitem S → pitem S
+ | po: pitem S → pitem S → pitem S
+ | pk: pitem S → pitem S.
+
+definition pre ≝ λS.pitem S × bool.
+
+interpretation "pitem star" 'star a = (pk ? a).
+interpretation "pitem or" 'plus a b = (po ? a b).
+interpretation "pitem cat" 'middot a b = (pc ? a b).
+notation < ".a" non associative with precedence 90 for @{ 'pp $a}.
+notation > "`. term 90 a" non associative with precedence 90 for @{ 'pp $a}.
+interpretation "pitem pp" 'pp a = (pp ? a).
+interpretation "pitem ps" 'ps a = (ps ? a).
+interpretation "pitem epsilon" 'epsilon = (pe ?).
+interpretation "pitem empty" 'empty = (pz ?).
+
+let rec forget (S: DeqSet) (l : pitem S) on l: re S ≝
+ match l with
+ [ pz ⇒ `∅
+ | pe ⇒ ϵ
+ | ps x ⇒ `x
+ | pp x ⇒ `x
+ | pc E1 E2 ⇒ (forget ? E1) · (forget ? E2)
+ | po E1 E2 ⇒ (forget ? E1) + (forget ? E2)
+ | pk E ⇒ (forget ? E)^* ].
+
+(* notation < "|term 19 e|" non associative with precedence 70 for @{'forget $e}.*)
+interpretation "forget" 'norm a = (forget ? a).
+
+lemma erase_dot : ∀S.∀e1,e2:pitem S. |e1 · e2| = c ? (|e1|) (|e2|).
+// qed.
+
+lemma erase_plus : ∀S.∀i1,i2:pitem S.
+ |i1 + i2| = |i1| + |i2|.
+// qed.
+
+lemma erase_star : ∀S.∀i:pitem S.|i^*| = |i|^*.
+// qed.
+
+(* boolean equality *)
+let rec beqitem S (i1,i2: pitem S) on i1 ≝
+ match i1 with
+ [ pz ⇒ match i2 with [ pz ⇒ true | _ ⇒ false]
+ | pe ⇒ match i2 with [ pe ⇒ true | _ ⇒ false]
+ | ps y1 ⇒ match i2 with [ ps y2 ⇒ y1==y2 | _ ⇒ false]
+ | pp y1 ⇒ match i2 with [ pp y2 ⇒ y1==y2 | _ ⇒ false]
+ | po i11 i12 ⇒ match i2 with
+ [ po i21 i22 ⇒ beqitem S i11 i21 ∧ beqitem S i12 i22
+ | _ ⇒ false]
+ | pc i11 i12 ⇒ match i2 with
+ [ pc i21 i22 ⇒ beqitem S i11 i21 ∧ beqitem S i12 i22
+ | _ ⇒ false]
+ | pk i11 ⇒ match i2 with [ pk i21 ⇒ beqitem S i11 i21 | _ ⇒ false]
+ ].
+
+lemma beqitem_true: ∀S,i1,i2. iff (beqitem S i1 i2 = true) (i1 = i2).
+#S #i1 elim i1
+ [#i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % // normalize #H destruct
+ |#i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % // normalize #H destruct
+ |#x #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % normalize #H destruct
+ [>(\P H) // | @(\b (refl …))]
+ |#x #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % normalize #H destruct
+ [>(\P H) // | @(\b (refl …))]
+ |#i11 #i12 #Hind1 #Hind2 #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] %
+ normalize #H destruct
+ [cases (true_or_false (beqitem S i11 i21)) #H1
+ [>(proj1 … (Hind1 i21) H1) >(proj1 … (Hind2 i22)) // >H1 in H; #H @H
+ |>H1 in H; normalize #abs @False_ind /2/
+ ]
+ |>(proj2 … (Hind1 i21) (refl …)) >(proj2 … (Hind2 i22) (refl …)) //
+ ]
+ |#i11 #i12 #Hind1 #Hind2 #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] %
+ normalize #H destruct
+ [cases (true_or_false (beqitem S i11 i21)) #H1
+ [>(proj1 … (Hind1 i21) H1) >(proj1 … (Hind2 i22)) // >H1 in H; #H @H
+ |>H1 in H; normalize #abs @False_ind /2/
+ ]
+ |>(proj2 … (Hind1 i21) (refl …)) >(proj2 … (Hind2 i22) (refl …)) //
+ ]
+ |#i3 #Hind #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i4] %
+ normalize #H destruct
+ [>(proj1 … (Hind i4) H) // |>(proj2 … (Hind i4) (refl …)) //]
+ ]
+qed.
+
+definition DeqItem ≝ λS.
+ mk_DeqSet (pitem S) (beqitem S) (beqitem_true S).
+
+unification hint 0 ≔ S;
+ X ≟ mk_DeqSet (pitem S) (beqitem S) (beqitem_true S)
+(* ---------------------------------------- *) ⊢
+ pitem S ≡ carr X.
+
+unification hint 0 ≔ S,i1,i2;
+ X ≟ mk_DeqSet (pitem S) (beqitem S) (beqitem_true S)
+(* ---------------------------------------- *) ⊢
+ beqitem S i1 i2 ≡ eqb X i1 i2.
+
+(* semantics *)
+
+let rec in_pl (S : DeqSet) (r : pitem S) on r : word S → Prop ≝
+match r with
+[ pz ⇒ ∅
+| pe ⇒ ∅
+| ps _ ⇒ ∅
+| pp x ⇒ { [x] }
+| pc r1 r2 ⇒ (in_pl ? r1) · \sem{forget ? r2} ∪ (in_pl ? r2)
+| po r1 r2 ⇒ (in_pl ? r1) ∪ (in_pl ? r2)
+| pk r1 ⇒ (in_pl ? r1) · \sem{forget ? r1}^* ].
+
+interpretation "in_pl" 'in_l E = (in_pl ? E).
+interpretation "in_pl mem" 'mem w l = (in_pl ? l w).
+
+definition in_prl ≝ λS : DeqSet.λp:pre S.
+ if (\snd p) then \sem{\fst p} ∪ {ϵ} else \sem{\fst p}.
+
+interpretation "in_prl mem" 'mem w l = (in_prl ? l w).
+interpretation "in_prl" 'in_l E = (in_prl ? E).
+
+lemma sem_pre_true : ∀S.∀i:pitem S.
+ \sem{〈i,true〉} = \sem{i} ∪ {ϵ}.
+// qed.
+
+lemma sem_pre_false : ∀S.∀i:pitem S.
+ \sem{〈i,false〉} = \sem{i}.
+// qed.
+
+lemma sem_cat: ∀S.∀i1,i2:pitem S.
+ \sem{i1 · i2} = \sem{i1} · \sem{|i2|} ∪ \sem{i2}.
+// qed.
+
+lemma sem_cat_w: ∀S.∀i1,i2:pitem S.∀w.
+ \sem{i1 · i2} w = ((\sem{i1} · \sem{|i2|}) w ∨ \sem{i2} w).
+// qed.
+
+lemma sem_plus: ∀S.∀i1,i2:pitem S.
+ \sem{i1 + i2} = \sem{i1} ∪ \sem{i2}.
+// qed.
+
+lemma sem_plus_w: ∀S.∀i1,i2:pitem S.∀w.
+ \sem{i1 + i2} w = (\sem{i1} w ∨ \sem{i2} w).
+// qed.
+
+lemma sem_star : ∀S.∀i:pitem S.
+ \sem{i^*} = \sem{i} · \sem{|i|}^*.
+// qed.
+
+lemma sem_star_w : ∀S.∀i:pitem S.∀w.
+ \sem{i^*} w = (∃w1,w2.w1 @ w2 = w ∧ \sem{i} w1 ∧ \sem{|i|}^* w2).
+// qed.
+
+lemma append_eq_nil : ∀S.∀w1,w2:word S. w1 @ w2 = ϵ → w1 = ϵ.
+#S #w1 #w2 cases w1 // #a #tl normalize #H destruct qed.
+
+lemma not_epsilon_lp : ∀S:DeqSet.∀e:pitem S. ¬ (ϵ ∈ e).
+#S #e elim e normalize /2/
+ [#r1 #r2 * #n1 #n2 % * /2/ * #w1 * #w2 * * #H
+ >(append_eq_nil …H…) /2/
+ |#r1 #r2 #n1 #n2 % * /2/
+ |#r #n % * #w1 * #w2 * * #H >(append_eq_nil …H…) /2/
+ ]
+qed.
+
+(* lemma 12 *)
+lemma epsilon_to_true : ∀S.∀e:pre S. ϵ ∈ e → \snd e = true.
+#S * #i #b cases b // normalize #H @False_ind /2/
+qed.
+
+lemma true_to_epsilon : ∀S.∀e:pre S. \snd e = true → ϵ ∈ e.
+#S * #i #b #btrue normalize in btrue; >btrue %2 //
+qed.
+
+lemma minus_eps_item: ∀S.∀i:pitem S. \sem{i} =1 \sem{i}-{[ ]}.
+#S #i #w %
+ [#H whd % // normalize @(not_to_not … (not_epsilon_lp …i)) //
+ |* //
+ ]
+qed.
+
+lemma minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
+#S * #i *
+ [>sem_pre_true normalize in ⊢ (??%?); #w %
+ [/3/ | * * // #H1 #H2 @False_ind @(absurd …H1 H2)]
+ |>sem_pre_false normalize in ⊢ (??%?); #w % [ /3/ | * // ]
+ ]
+qed.
+
+definition lo ≝ λS:DeqSet.λa,b:pre S.〈\fst a + \fst b,\snd a ∨ \snd b〉.
+notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}.
+interpretation "oplus" 'oplus a b = (lo ? a b).
+
+lemma lo_def: ∀S.∀i1,i2:pitem S.∀b1,b2. 〈i1,b1〉⊕〈i2,b2〉=〈i1+i2,b1∨b2〉.
+// qed.
+
+definition pre_concat_r ≝ λS:DeqSet.λi:pitem S.λe:pre S.
+ match e with [ mk_Prod i1 b ⇒ 〈i · i1, b〉].
+
+notation "i ◃ e" left associative with precedence 60 for @{'lhd $i $e}.
+interpretation "pre_concat_r" 'lhd i e = (pre_concat_r ? i e).
+
+lemma eq_to_ex_eq: ∀S.∀A,B:word S → Prop.
+ A = B → A =1 B.
+#S #A #B #H >H /2/ qed.
+
+lemma sem_pre_concat_r : ∀S,i.∀e:pre S.
+ \sem{i ◃ e} =1 \sem{i} · \sem{|\fst e|} ∪ \sem{e}.
+#S #i * #i1 #b1 cases b1 [2: @eq_to_ex_eq //]
+>sem_pre_true >sem_cat >sem_pre_true /2/
+qed.
+
+definition pre_concat_l ≝ λS:DeqSet.λbcast:∀S:DeqSet.pitem S → pre S.λe1:pre S.λi2:pitem S.
+ match e1 with
+ [ mk_Prod i1 b1 ⇒ match b1 with
+ [ true ⇒ (i1 ◃ (bcast ? i2))
+ | false ⇒ 〈i1 · i2,false〉
+ ]
+ ].
+
+notation "a ▹ b" left associative with precedence 60 for @{'tril eclose $a $b}.
+interpretation "item-pre concat" 'tril op a b = (pre_concat_l ? op a b).
+
+notation "•" non associative with precedence 60 for @{eclose ?}.
+
+let rec eclose (S: DeqSet) (i: pitem S) on i : pre S ≝
+ match i with
+ [ pz ⇒ 〈 `∅, false 〉
+ | pe ⇒ 〈 ϵ, true 〉
+ | ps x ⇒ 〈 `.x, false〉
+ | pp x ⇒ 〈 `.x, false 〉
+ | po i1 i2 ⇒ •i1 ⊕ •i2
+ | pc i1 i2 ⇒ •i1 ▹ i2
+ | pk i ⇒ 〈(\fst (•i))^*,true〉].
+
+notation "• x" non associative with precedence 60 for @{'eclose $x}.
+interpretation "eclose" 'eclose x = (eclose ? x).
+
+lemma eclose_plus: ∀S:DeqSet.∀i1,i2:pitem S.
+ •(i1 + i2) = •i1 ⊕ •i2.
+// qed.
+
+lemma eclose_dot: ∀S:DeqSet.∀i1,i2:pitem S.
+ •(i1 · i2) = •i1 ▹ i2.
+// qed.
+
+lemma eclose_star: ∀S:DeqSet.∀i:pitem S.
+ •i^* = 〈(\fst(•i))^*,true〉.
+// qed.
+
+definition lift ≝ λS.λf:pitem S →pre S.λe:pre S.
+ match e with
+ [ mk_Prod i b ⇒ 〈\fst (f i), \snd (f i) ∨ b〉].
+
+definition preclose ≝ λS. lift S (eclose S).
+interpretation "preclose" 'eclose x = (preclose ? x).
+
+(* theorem 16: 2 *)
+lemma sem_oplus: ∀S:DeqSet.∀e1,e2:pre S.
+ \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}.
+#S * #i1 #b1 * #i2 #b2 #w %
+ [cases b1 cases b2 normalize /2/ * /3/ * /3/
+ |cases b1 cases b2 normalize /2/ * /3/ * /3/
+ ]
+qed.
+
+lemma odot_true :
+ ∀S.∀i1,i2:pitem S.
+ 〈i1,true〉 ▹ i2 = i1 ◃ (•i2).
+// qed.
+
+lemma odot_true_bis :
+ ∀S.∀i1,i2:pitem S.
+ 〈i1,true〉 ▹ i2 = 〈i1 · \fst (•i2), \snd (•i2)〉.
+#S #i1 #i2 normalize cases (•i2) // qed.
+
+lemma odot_false:
+ ∀S.∀i1,i2:pitem S.
+ 〈i1,false〉 ▹ i2 = 〈i1 · i2, false〉.
+// qed.
+
+lemma LcatE : ∀S.∀e1,e2:pitem S.
+ \sem{e1 · e2} = \sem{e1} · \sem{|e2|} ∪ \sem{e2}.
+// qed.
+
+lemma erase_bull : ∀S.∀i:pitem S. |\fst (•i)| = |i|.
+#S #i elim i //
+ [ #i1 #i2 #IH1 #IH2 >erase_dot <IH1 >eclose_dot
+ cases (•i1) #i11 #b1 cases b1 // <IH2 >odot_true_bis //
+ | #i1 #i2 #IH1 #IH2 >eclose_plus >(erase_plus … i1) <IH1 <IH2
+ cases (•i1) #i11 #b1 cases (•i2) #i21 #b2 //
+ | #i #IH >eclose_star >(erase_star … i) <IH cases (•i) //
+ ]
+qed.
+
+(*
+lemma sem_eclose_star: ∀S:DeqSet.∀i:pitem S.
+ \sem{〈i^*,true〉} =1 \sem{〈i,false〉}·\sem{|i|}^* ∪ {ϵ}.
+/2/ qed.
+*)
+
+(* theorem 16: 1 → 3 *)
+lemma odot_dot_aux : ∀S.∀e1:pre S.∀i2:pitem S.
+ \sem{•i2} =1 \sem{i2} ∪ \sem{|i2|} →
+ \sem{e1 ▹ i2} =1 \sem{e1} · \sem{|i2|} ∪ \sem{i2}.
+#S * #i1 #b1 #i2 cases b1
+ [2:#th >odot_false >sem_pre_false >sem_pre_false >sem_cat /2/
+ |#H >odot_true >sem_pre_true @(eqP_trans … (sem_pre_concat_r …))
+ >erase_bull @eqP_trans [|@(eqP_union_l … H)]
+ @eqP_trans [|@eqP_union_l[|@union_comm ]]
+ @eqP_trans [|@eqP_sym @union_assoc ] /3/
+ ]
+qed.
+
+lemma minus_eps_pre_aux: ∀S.∀e:pre S.∀i:pitem S.∀A.
+ \sem{e} =1 \sem{i} ∪ A → \sem{\fst e} =1 \sem{i} ∪ (A - {[ ]}).
+#S #e #i #A #seme
+@eqP_trans [|@minus_eps_pre]
+@eqP_trans [||@eqP_union_r [|@eqP_sym @minus_eps_item]]
+@eqP_trans [||@distribute_substract]
+@eqP_substract_r //
+qed.
+
+(* theorem 16: 1 *)
+theorem sem_bull: ∀S:DeqSet. ∀i:pitem S. \sem{•i} =1 \sem{i} ∪ \sem{|i|}.
+#S #e elim e
+ [#w normalize % [/2/ | * //]
+ |/2/
+ |#x normalize #w % [ /2/ | * [@False_ind | //]]
+ |#x normalize #w % [ /2/ | * // ]
+ |#i1 #i2 #IH1 #IH2 >eclose_dot
+ @eqP_trans [|@odot_dot_aux //] >sem_cat
+ @eqP_trans
+ [|@eqP_union_r
+ [|@eqP_trans [|@(cat_ext_l … IH1)] @distr_cat_r]]
+ @eqP_trans [|@union_assoc]
+ @eqP_trans [||@eqP_sym @union_assoc]
+ @eqP_union_l //
+ |#i1 #i2 #IH1 #IH2 >eclose_plus
+ @eqP_trans [|@sem_oplus] >sem_plus >erase_plus
+ @eqP_trans [|@(eqP_union_l … IH2)]
+ @eqP_trans [|@eqP_sym @union_assoc]
+ @eqP_trans [||@union_assoc] @eqP_union_r
+ @eqP_trans [||@eqP_sym @union_assoc]
+ @eqP_trans [||@eqP_union_l [|@union_comm]]
+ @eqP_trans [||@union_assoc] /2/
+ |#i #H >sem_pre_true >sem_star >erase_bull >sem_star
+ @eqP_trans [|@eqP_union_r [|@cat_ext_l [|@minus_eps_pre_aux //]]]
+ @eqP_trans [|@eqP_union_r [|@distr_cat_r]]
+ @eqP_trans [|@union_assoc] @eqP_union_l >erase_star
+ @eqP_sym @star_fix_eps
+ ]
+qed.
+
+(* blank item *)
+let rec blank (S: DeqSet) (i: re S) on i :pitem S ≝
+ match i with
+ [ z ⇒ `∅
+ | e ⇒ ϵ
+ | s y ⇒ `y
+ | o e1 e2 ⇒ (blank S e1) + (blank S e2)
+ | c e1 e2 ⇒ (blank S e1) · (blank S e2)
+ | k e ⇒ (blank S e)^* ].
+
+lemma forget_blank: ∀S.∀e:re S.|blank S e| = e.
+#S #e elim e normalize //
+qed.
+
+lemma sem_blank: ∀S.∀e:re S.\sem{blank S e} =1 ∅.
+#S #e elim e
+ [1,2:@eq_to_ex_eq //
+ |#s @eq_to_ex_eq //
+ |#e1 #e2 #Hind1 #Hind2 >sem_cat
+ @eqP_trans [||@(union_empty_r … ∅)]
+ @eqP_trans [|@eqP_union_l[|@Hind2]] @eqP_union_r
+ @eqP_trans [||@(cat_empty_l … ?)] @cat_ext_l @Hind1
+ |#e1 #e2 #Hind1 #Hind2 >sem_plus
+ @eqP_trans [||@(union_empty_r … ∅)]
+ @eqP_trans [|@eqP_union_l[|@Hind2]] @eqP_union_r @Hind1
+ |#e #Hind >sem_star
+ @eqP_trans [||@(cat_empty_l … ?)] @cat_ext_l @Hind
+ ]
+qed.
+
+theorem re_embedding: ∀S.∀e:re S.
+ \sem{•(blank S e)} =1 \sem{e}.
+#S #e @eqP_trans [|@sem_bull] >forget_blank
+@eqP_trans [|@eqP_union_r [|@sem_blank]]
+@eqP_trans [|@union_comm] @union_empty_r.
+qed.
+
+(* lefted operations *)
+definition lifted_cat ≝ λS:DeqSet.λe:pre S.
+ lift S (pre_concat_l S eclose e).
+
+notation "e1 ⊙ e2" left associative with precedence 70 for @{'odot $e1 $e2}.
+
+interpretation "lifted cat" 'odot e1 e2 = (lifted_cat ? e1 e2).
+
+lemma odot_true_b : ∀S.∀i1,i2:pitem S.∀b.
+ 〈i1,true〉 ⊙ 〈i2,b〉 = 〈i1 · (\fst (•i2)),\snd (•i2) ∨ b〉.
+#S #i1 #i2 #b normalize in ⊢ (??%?); cases (•i2) //
+qed.
+
+lemma odot_false_b : ∀S.∀i1,i2:pitem S.∀b.
+ 〈i1,false〉 ⊙ 〈i2,b〉 = 〈i1 · i2 ,b〉.
+//
+qed.
+
+lemma erase_odot:∀S.∀e1,e2:pre S.
+ |\fst (e1 ⊙ e2)| = |\fst e1| · (|\fst e2|).
+#S * #i1 * * #i2 #b2 // >odot_true_b >erase_dot //
+qed.
+
+definition lk ≝ λS:DeqSet.λe:pre S.
+ match e with
+ [ mk_Prod i1 b1 ⇒
+ match b1 with
+ [true ⇒ 〈(\fst (eclose ? i1))^*, true〉
+ |false ⇒ 〈i1^*,false〉
+ ]
+ ].
+
+(* notation < "a \sup ⊛" non associative with precedence 90 for @{'lk $a}.*)
+interpretation "lk" 'lk a = (lk ? a).
+notation "a^⊛" non associative with precedence 90 for @{'lk $a}.
+
+
+lemma ostar_true: ∀S.∀i:pitem S.
+ 〈i,true〉^⊛ = 〈(\fst (•i))^*, true〉.
+// qed.
+
+lemma ostar_false: ∀S.∀i:pitem S.
+ 〈i,false〉^⊛ = 〈i^*, false〉.
+// qed.
+
+lemma erase_ostar: ∀S.∀e:pre S.
+ |\fst (e^⊛)| = |\fst e|^*.
+#S * #i * // qed.
+
+lemma sem_odot_true: ∀S:DeqSet.∀e1:pre S.∀i.
+ \sem{e1 ⊙ 〈i,true〉} =1 \sem{e1 ▹ i} ∪ { [ ] }.
+#S #e1 #i
+cut (e1 ⊙ 〈i,true〉 = 〈\fst (e1 ▹ i), \snd(e1 ▹ i) ∨ true〉) [//]
+#H >H cases (e1 ▹ i) #i1 #b1 cases b1
+ [>sem_pre_true @eqP_trans [||@eqP_sym @union_assoc]
+ @eqP_union_l /2/
+ |/2/
+ ]
+qed.
+
+lemma eq_odot_false: ∀S:DeqSet.∀e1:pre S.∀i.
+ e1 ⊙ 〈i,false〉 = e1 ▹ i.
+#S #e1 #i
+cut (e1 ⊙ 〈i,false〉 = 〈\fst (e1 ▹ i), \snd(e1 ▹ i) ∨ false〉) [//]
+cases (e1 ▹ i) #i1 #b1 cases b1 #H @H
+qed.
+
+lemma sem_odot:
+ ∀S.∀e1,e2: pre S. \sem{e1 ⊙ e2} =1 \sem{e1}· \sem{|\fst e2|} ∪ \sem{e2}.
+#S #e1 * #i2 *
+ [>sem_pre_true
+ @eqP_trans [|@sem_odot_true]
+ @eqP_trans [||@union_assoc] @eqP_union_r @odot_dot_aux //
+ |>sem_pre_false >eq_odot_false @odot_dot_aux //
+ ]
+qed.
+
+(* theorem 16: 4 *)
+theorem sem_ostar: ∀S.∀e:pre S.
+ \sem{e^⊛} =1 \sem{e} · \sem{|\fst e|}^*.
+#S * #i #b cases b
+ [>sem_pre_true >sem_pre_true >sem_star >erase_bull
+ @eqP_trans [|@eqP_union_r[|@cat_ext_l [|@minus_eps_pre_aux //]]]
+ @eqP_trans [|@eqP_union_r [|@distr_cat_r]]
+ @eqP_trans [||@eqP_sym @distr_cat_r]
+ @eqP_trans [|@union_assoc] @eqP_union_l
+ @eqP_trans [||@eqP_sym @epsilon_cat_l] @eqP_sym @star_fix_eps
+ |>sem_pre_false >sem_pre_false >sem_star /2/
+ ]
+qed.
+
--- /dev/null
+baseuri=cic:/matita/
projects / helm.git / commitdiff