From 0d481cc22ba8ada5781885da5398086a0b5662f3 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 10 Jan 2012 08:31:46 +0000 Subject: [PATCH] A complete snapshot for re --- matita/matita/lib/re/moves.ma | 5 +- matita/matita/re_complete/basics/bool.ma | 95 ++++ .../re_complete/basics/core_notation.ma | 318 +++++++++++ matita/matita/re_complete/basics/deqsets.ma | 92 +++ .../re_complete/basics/hints_declaration.ma | 93 ++++ matita/matita/re_complete/basics/list.ma | 322 +++++++++++ matita/matita/re_complete/basics/listb.ma | 215 +++++++ matita/matita/re_complete/basics/logic.ma | 261 +++++++++ matita/matita/re_complete/basics/nat.ma | 271 +++++++++ matita/matita/re_complete/basics/pts.ma | 7 + matita/matita/re_complete/basics/relations.ma | 82 +++ matita/matita/re_complete/basics/sets.ma | 107 ++++ matita/matita/re_complete/basics/types.ma | 212 +++++++ matita/matita/re_complete/lang.ma | 132 +++++ matita/matita/re_complete/moves.ma | 485 ++++++++++++++++ matita/matita/re_complete/re.ma | 525 ++++++++++++++++++ matita/matita/re_complete/root | 1 + 17 files changed, 3222 insertions(+), 1 deletion(-) create mode 100644 matita/matita/re_complete/basics/bool.ma create mode 100644 matita/matita/re_complete/basics/core_notation.ma create mode 100644 matita/matita/re_complete/basics/deqsets.ma create mode 100644 matita/matita/re_complete/basics/hints_declaration.ma create mode 100644 matita/matita/re_complete/basics/list.ma create mode 100644 matita/matita/re_complete/basics/listb.ma create mode 100644 matita/matita/re_complete/basics/logic.ma create mode 100644 matita/matita/re_complete/basics/nat.ma create mode 100644 matita/matita/re_complete/basics/pts.ma create mode 100644 matita/matita/re_complete/basics/relations.ma create mode 100644 matita/matita/re_complete/basics/sets.ma create mode 100644 matita/matita/re_complete/basics/types.ma create mode 100644 matita/matita/re_complete/lang.ma create mode 100644 matita/matita/re_complete/moves.ma create mode 100644 matita/matita/re_complete/re.ma create mode 100644 matita/matita/re_complete/root diff --git a/matita/matita/lib/re/moves.ma b/matita/matita/lib/re/moves.ma index f4da274a6..6e4dbb974 100644 --- a/matita/matita/lib/re/moves.ma +++ b/matita/matita/lib/re/moves.ma @@ -497,8 +497,11 @@ definition exp9 ≝ (a·a·a + a·a·a·a·a)^*. 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. diff --git a/matita/matita/re_complete/basics/bool.ma b/matita/matita/re_complete/basics/bool.ma new file mode 100644 index 000000000..028891251 --- /dev/null +++ b/matita/matita/re_complete/basics/bool.ma @@ -0,0 +1,95 @@ +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. + + diff --git a/matita/matita/re_complete/basics/core_notation.ma b/matita/matita/re_complete/basics/core_notation.ma new file mode 100644 index 000000000..4eae6c6c3 --- /dev/null +++ b/matita/matita/re_complete/basics/core_notation.ma @@ -0,0 +1,318 @@ +(* 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}. diff --git a/matita/matita/re_complete/basics/deqsets.ma b/matita/matita/re_complete/basics/deqsets.ma new file mode 100644 index 000000000..4a69be36f --- /dev/null +++ b/matita/matita/re_complete/basics/deqsets.ma @@ -0,0 +1,92 @@ +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 (\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 diff --git a/matita/matita/re_complete/basics/hints_declaration.ma b/matita/matita/re_complete/basics/hints_declaration.ma new file mode 100644 index 000000000..ee9487d54 --- /dev/null +++ b/matita/matita/re_complete/basics/hints_declaration.ma @@ -0,0 +1,93 @@ +(* + +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 diff --git a/matita/matita/re_complete/basics/list.ma b/matita/matita/re_complete/basics/list.ma new file mode 100644 index 000000000..b0a683135 --- /dev/null +++ b/matita/matita/re_complete/basics/list.ma @@ -0,0 +1,322 @@ +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 (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 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. diff --git a/matita/matita/re_complete/basics/logic.ma b/matita/matita/re_complete/basics/logic.ma new file mode 100644 index 000000000..e2c93a410 --- /dev/null +++ b/matita/matita/re_complete/basics/logic.ma @@ -0,0 +1,261 @@ +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. diff --git a/matita/matita/re_complete/basics/nat.ma b/matita/matita/re_complete/basics/nat.ma new file mode 100644 index 000000000..033193ee4 --- /dev/null +++ b/matita/matita/re_complete/basics/nat.ma @@ -0,0 +1,271 @@ +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 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 ??)). diff --git a/matita/matita/re_complete/lang.ma b/matita/matita/re_complete/lang.ma new file mode 100644 index 000000000..430fc3f21 --- /dev/null +++ b/matita/matita/re_complete/lang.ma @@ -0,0 +1,132 @@ +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 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] 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

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 (bisim_step_true … ptest) @HI -HI + [(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 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)〉) + [(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. + + + + + + + diff --git a/matita/matita/re_complete/re.ma b/matita/matita/re_complete/re.ma new file mode 100644 index 000000000..ff1f95993 --- /dev/null +++ b/matita/matita/re_complete/re.ma @@ -0,0 +1,525 @@ +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 eclose_dot + cases (•i1) #i11 #b1 cases b1 // odot_true_bis // + | #i1 #i2 #IH1 #IH2 >eclose_plus >(erase_plus … i1) eclose_star >(erase_star … i) 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. + diff --git a/matita/matita/re_complete/root b/matita/matita/re_complete/root new file mode 100644 index 000000000..c57405b94 --- /dev/null +++ b/matita/matita/re_complete/root @@ -0,0 +1 @@ +baseuri=cic:/matita/ -- 2.39.2