From: Claudio Sacerdoti Coen Date: Mon, 12 Dec 2011 16:52:47 +0000 (+0000) Subject: Pairs are now records. X-Git-Tag: make_still_working~2025 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bf5696fc20ffbe552ecb1cd8af0d6fc78d1de9e8;p=helm.git Pairs are now records. Pros: projections from concrete records are now automatically reduced away. Cons: the name of the constructor is no longer pair, but mk_Prod. --- diff --git a/matita/matita/lib/basics/types.ma b/matita/matita/lib/basics/types.ma index f35dde531..2852662e4 100644 --- a/matita/matita/lib/basics/types.ma +++ b/matita/matita/lib/basics/types.ma @@ -18,19 +18,15 @@ inductive void : Type[0] ≝. inductive unit : Type[0] ≝ it: unit. (* Prod *) -inductive Prod (A,B:Type[0]) : Type[0] ≝ -pair : A → B → Prod A B. +record Prod (A,B:Type[0]) : Type[0] ≝ { + fst: A + ; snd: B + }. -interpretation "Pair construction" 'pair x y = (pair ? ? x y). +interpretation "Pair construction" 'pair x y = (mk_Prod ? ? x y). interpretation "Product" 'product x y = (Prod x y). -definition fst ≝ λA,B.λp:A × B. - match p with [pair a b ⇒ a]. - -definition snd ≝ λA,B.λp:A × B. - match p with [pair a b ⇒ b]. - interpretation "pair pi1" 'pi1 = (fst ? ?). interpretation "pair pi2" 'pi2 = (snd ? ?). interpretation "pair pi1" 'pi1a x = (fst ? ? x). diff --git a/matita/matita/lib/re/moves.ma b/matita/matita/lib/re/moves.ma index b2f53bb6f..b7f094d86 100644 --- a/matita/matita/lib/re/moves.ma +++ b/matita/matita/lib/re/moves.ma @@ -115,7 +115,7 @@ lemma moves_cons: ∀S:DeqSet.∀a:S.∀w.∀e:pre S. 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 >fst_eq cases b normalize +#S #a #w * #i #b cases b normalize [% /2/ * // #H destruct |% normalize /2/] qed. @@ -371,7 +371,7 @@ lemma bisim_ok1: ∀S.∀e1,e2:pre S.\sem{e1}=1\sem{e2} → @le_to_not_lt @sublist_length // * #e11 #e21 #membp cut ((|\fst e11| = |\fst e1|) ∧ (|\fst e21| = |\fst e2|)) [|* #H1 #H2

fst_eq >snd_eq #we1 #we2 #_ + cases (H … membp) * #w * #we1 #we2 #_ bisim_end //] #p #front_tl #visited #Hn * #u_visited #vinv * #u_frontier #finv @@ -622,7 +622,7 @@ cases (reachable_bisim … allH init … H) * #H1 #H2 #H3 cut (∀w.sublist ? w (occ S e1 e2)→∀p.memb (space S) p visited_res = true → memb (space S) 〈moves ? w (\fst p), moves ? w (\snd p)〉 visited_res = true) [#w elim w [//] - #a #w1 #Hind #Hsub * #e11 #e21 #visp >fst_eq >snd_eq >moves_cons >moves_cons + #a #w1 #Hind #Hsub * #e11 #e21 #visp >moves_cons >moves_cons @(Hind ? 〈?,?〉) [#x #H4 @Hsub @memb_cons //] @(H1 〈?,?〉) // @Hsub @memb_hd] #all_reach @bisim_char @occ_enough diff --git a/matita/matita/lib/re/re.ma b/matita/matita/lib/re/re.ma index 1357bbb5b..1695575f0 100644 --- a/matita/matita/lib/re/re.ma +++ b/matita/matita/lib/re/re.ma @@ -218,7 +218,7 @@ lemma lo_def: ∀S.∀i1,i2:pitem S.∀b1,b2. 〈i1,b1〉⊕〈i2,b2〉=〈i1+i2 // qed. definition pre_concat_r ≝ λS:DeqSet.λi:pitem S.λe:pre S. - match e with [ pair i1 b ⇒ 〈i · i1, b〉]. + match e with [ mk_Prod i1 b ⇒ 〈i · i1, b〉]. notation "i ◂ e" left associative with precedence 60 for @{'ltrif $i $e}. interpretation "pre_concat_r" 'ltrif i e = (pre_concat_r ? i e). @@ -239,7 +239,7 @@ qed. definition lc ≝ λS:DeqSet.λbcast:∀S:DeqSet.pitem S → pre S.λe1:pre S.λi2:pitem S. match e1 with - [ pair i1 b1 ⇒ match b1 with + [ mk_Prod i1 b1 ⇒ match b1 with [ true ⇒ (i1 ◂ (bcast ? i2)) | false ⇒ 〈i1 · i2,false〉 ] @@ -247,14 +247,14 @@ definition lc ≝ λS:DeqSet.λbcast:∀S:DeqSet.pitem S → pre S.λe1:pre S.λ definition lift ≝ λS.λf:pitem S →pre S.λe:pre S. match e with - [ pair i b ⇒ 〈\fst (f i), \snd (f i) ∨ b〉]. + [ mk_Prod i b ⇒ 〈\fst (f i), \snd (f i) ∨ b〉]. notation "a ▸ b" left associative with precedence 60 for @{'lc eclose $a $b}. interpretation "lc" 'lc op a b = (lc ? op a b). definition lk ≝ λS:DeqSet.λbcast:∀S:DeqSet.∀E:pitem S.pre S.λe:pre S. match e with - [ pair i1 b1 ⇒ + [ mk_Prod i1 b1 ⇒ match b1 with [true ⇒ 〈(\fst (bcast ? i1))^*, true〉 |false ⇒ 〈i1^*,false〉 @@ -553,7 +553,7 @@ qed. lemma erase_odot:∀S.∀e1,e2:pre S. |\fst (e1 ⊙ e2)| = |\fst e1| · (|\fst e2|). -#S * #i1 * * #i2 #b2 // >odot_true_b >fst_eq >fst_eq >fst_eq // +#S * #i1 * * #i2 #b2 // >odot_true_b // qed. lemma ostar_true: ∀S.∀i:pitem S. diff --git a/matita/matita/lib/re/reb.ma b/matita/matita/lib/re/reb.ma index 7dbf69e13..79a74c24d 100644 --- a/matita/matita/lib/re/reb.ma +++ b/matita/matita/lib/re/reb.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "arithmetics/nat.ma". -include "basics/list.ma". +include "basics/lists/list.ma". interpretation "iff" 'iff a b = (iff a b).