From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
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 <H1 <H2 @space_enum_complete]
-   cases (H … membp) * #w * >fst_eq >snd_eq #we1 #we2 #_
+   cases (H … membp) * #w * #we1 #we2 #_
    <we1 <we2 % //    
   |#m #HI * [#visited #vinv #finv >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).