From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 22 Jul 2009 15:10:50 +0000 (+0000)
Subject: 1) PTS simplified
X-Git-Tag: make_still_working~3633
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=33b04453963755b619ac644f988e86a09cd54d63;p=helm.git

1) PTS simplified
2) several eliminiation principles and projections are now automatically generated
---

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma
index 7d6006862..87a166d17 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma
@@ -40,13 +40,13 @@ ndefinition bool_destruct : bool_destruct_aux.
  nelim b2;
  nnormalize;
  #H;
- ##[ ##2: napply (False_ind (λx.P) ?);
+ ##[ ##2: napply (False_ind (λx.?) ?);
           (* perche' non napply (False_ind ??); !!! *)
           nchange with (match true with [ true ⇒ False | false ⇒ True]);
           nrewrite > H;
           nnormalize;
           napply I
- ##| ##3: napply (False_ind (λx.P) ?);
+ ##| ##3: napply (False_ind (λx.?) ?);
           (* perche' non napply (False_ind ??); !!! *)
           nchange with (match true with [ true ⇒ False | false ⇒ True]);
           nrewrite < H;
diff --git a/helm/software/matita/contribs/ng_assembly/freescale/byte8.ma b/helm/software/matita/contribs/ng_assembly/freescale/byte8.ma
index ce9068703..ed4a47ea3 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/byte8.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/byte8.ma
@@ -32,7 +32,7 @@ nrecord byte8 : Type ≝
  b8l: exadecim
  }.
 
-ndefinition byte8_ind : ΠP:byte8 → Prop.(Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1)) → Πb:byte8.P b ≝
+(*ndefinition byte8_ind : ΠP:byte8 → Prop.(Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1)) → Πb:byte8.P b ≝
 λP:byte8 → Prop.λf:Πe:exadecim.Πe1:exadecim.P (mk_byte8 e e1).λb:byte8.
  match b with [ mk_byte8 (e:exadecim) (e1:exadecim) ⇒ f e e1 ].
 
@@ -45,7 +45,7 @@ ndefinition byte8_rect : ΠP:byte8 → Type.(Πe:exadecim.Πe1:exadecim.P (mk_by
  match b with [ mk_byte8 (e:exadecim) (e1:exadecim) ⇒ f e e1 ].
 
 ndefinition b8h ≝ λb:byte8.match b with [ mk_byte8 x _ ⇒ x ].
-ndefinition b8l ≝ λb:byte8.match b with [ mk_byte8 _ x ⇒ x ].
+ndefinition b8l ≝ λb:byte8.match b with [ mk_byte8 _ x ⇒ x ].*)
 
 (* \langle \rangle *)
 notation "〈x,y〉" non associative with precedence 80
diff --git a/helm/software/matita/contribs/ng_assembly/freescale/option.ma b/helm/software/matita/contribs/ng_assembly/freescale/option.ma
index bcd66d441..4c7a9abb4 100644
--- a/helm/software/matita/contribs/ng_assembly/freescale/option.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/option.ma
@@ -30,7 +30,7 @@ ninductive option (A:Type) : Type ≝
   None : option A
 | Some : A → option A.
 
-ndefinition option_ind : ΠA:Type.ΠP:option A → Prop.P (None A) → (Πa:A.P (Some A a)) → Πop:option A.P op ≝
+(*ndefinition option_ind : ΠA:Type.ΠP:option A → Prop.P (None A) → (Πa:A.P (Some A a)) → Πop:option A.P op ≝
 λA:Type.λP:option A → Prop.λp:P (None A).λf:Πa:A.P (Some A a).λop:option A.
  match op with [ None ⇒ p | Some (a:A) ⇒ f a ].
 
@@ -40,7 +40,7 @@ ndefinition option_rec : ΠA:Type.ΠP:option A → Set.P (None A) → (Πa:A.P (
 
 ndefinition option_rect : ΠA:Type.ΠP:option A → Type.P (None A) → (Πa:A.P (Some A a)) → Πop:option A.P op ≝
 λA:Type.λP:option A → Type.λp:P (None A).λf:Πa:A.P (Some A a).λop:option A.
- match op with [ None ⇒ p | Some (a:A) ⇒ f a ].
+ match op with [ None ⇒ p | Some (a:A) ⇒ f a ].*)
 
 ndefinition eq_option ≝
 λT.λop1,op2:option T.λf:T → T → bool.
diff --git a/helm/software/matita/contribs/ng_assembly/freescale/pts.ma b/helm/software/matita/contribs/ng_assembly/freescale/pts.ma
index 8b57df603..1b00cc124 100644
--- a/helm/software/matita/contribs/ng_assembly/freescale/pts.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/pts.ma
@@ -20,11 +20,4 @@
 (*                                                                        *)
 (* ********************************************************************** *)
 
-universe constraint Type[0] < Type[1].
-universe constraint Type[1] < Type[2].
-universe constraint CProp[0] < CProp[1].
-universe constraint Type[0] ≤ CProp[0].
-universe constraint CProp[0] ≤ Type[0].
-universe constraint Type[1] ≤ CProp[1].
-universe constraint CProp[1] ≤ Type[1].
-
+universe constraint Type[0] < Type[1].
\ No newline at end of file
diff --git a/helm/software/matita/contribs/ng_assembly/freescale/word16.ma b/helm/software/matita/contribs/ng_assembly/freescale/word16.ma
index 90ebbe8ae..53d798b35 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/word16.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/word16.ma
@@ -32,7 +32,7 @@ nrecord word16 : Type ≝
  w16l: byte8
  }.
 
-ndefinition word16_ind : ΠP:word16 → Prop.(Πb:byte8.Πb1:byte8.P (mk_word16 b b1)) → Πw:word16.P w ≝
+(*ndefinition word16_ind : ΠP:word16 → Prop.(Πb:byte8.Πb1:byte8.P (mk_word16 b b1)) → Πw:word16.P w ≝
 λP:word16 → Prop.λf:Πb:byte8.Πb1:byte8.P (mk_word16 b b1).λw:word16.
  match w with [ mk_word16 (b:byte8) (b1:byte8) ⇒ f b b1 ].
 
@@ -45,7 +45,7 @@ ndefinition word16_rect : ΠP:word16 → Type.(Πb:byte8.Πb1:byte8.P (mk_word16
  match w with [ mk_word16 (b:byte8) (b1:byte8) ⇒ f b b1 ].
 
 ndefinition w16h ≝ λw:word16.match w with [ mk_word16 x _ ⇒ x ].
-ndefinition w16l ≝ λw:word16.match w with [ mk_word16 _ x ⇒ x ].
+ndefinition w16l ≝ λw:word16.match w with [ mk_word16 _ x ⇒ x ].*)
 
 (* \langle \rangle *)
 notation "〈x:y〉" non associative with precedence 80
diff --git a/helm/software/matita/contribs/ng_assembly/freescale/word32.ma b/helm/software/matita/contribs/ng_assembly/freescale/word32.ma
index 886afc65c..2e0dd8bac 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/word32.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/word32.ma
@@ -32,7 +32,7 @@ nrecord word32 : Type ≝
  w32l: word16
  }.
 
-ndefinition word32_ind : ΠP:word32 → Prop.(Πw:word16.Πw1:word16.P (mk_word32 w w1)) → Πdw:word32.P dw ≝
+(*ndefinition word32_ind : ΠP:word32 → Prop.(Πw:word16.Πw1:word16.P (mk_word32 w w1)) → Πdw:word32.P dw ≝
 λP:word32 → Prop.λf:Πw:word16.Πw1:word16.P (mk_word32 w w1).λdw:word32.
  match dw with [ mk_word32 (w:word16) (w1:word16) ⇒ f w w1 ].
 
@@ -45,7 +45,7 @@ ndefinition word32_rect : ΠP:word32 → Type.(Πw:word16.Πw1:word16.P (mk_word
  match dw with [ mk_word32 (w:word16) (w1:word16) ⇒ f w w1 ].
 
 ndefinition w32h ≝ λdw:word32.match dw with [ mk_word32 x _ ⇒ x ].
-ndefinition w32l ≝ λdw:word32.match dw with [ mk_word32 _ x ⇒ x ].
+ndefinition w32l ≝ λdw:word32.match dw with [ mk_word32 _ x ⇒ x ].*)
 
 (* \langle \rangle *)
 notation "〈x.y〉" non associative with precedence 80
diff --git a/helm/software/matita/contribs/ng_assembly/utility/ascii.ma b/helm/software/matita/contribs/ng_assembly/utility/ascii.ma
index 7a7d33793..35894f570 100755
--- a/helm/software/matita/contribs/ng_assembly/utility/ascii.ma
+++ b/helm/software/matita/contribs/ng_assembly/utility/ascii.ma
@@ -124,32 +124,6 @@ ndefinition ascii_ind
   | ch_l ⇒ p48 | ch_m ⇒ p49 | ch_n ⇒ p50 | ch_o ⇒ p51 | ch_p ⇒ p52 | ch_q ⇒ p53 | ch_r ⇒ p54 | ch_s ⇒ p55
   | ch_t ⇒ p56 | ch_u ⇒ p57 | ch_v ⇒ p58 | ch_w ⇒ p59 | ch_x ⇒ p60 | ch_y ⇒ p61 | ch_z ⇒ p62 ].
 
-ndefinition ascii_rec
- : ΠP:ascii → Set.
-   P ch_0 → P ch_1 → P ch_2 → P ch_3 → P ch_4 → P ch_5 → P ch_6 → P ch_7 → P ch_8 → P ch_9 → P ch__ →
-   P ch_A → P ch_B → P ch_C → P ch_D → P ch_E → P ch_F → P ch_G → P ch_H → P ch_I → P ch_J → P ch_K →
-   P ch_L → P ch_M → P ch_N → P ch_O → P ch_P → P ch_Q → P ch_R → P ch_S → P ch_T → P ch_U → P ch_V →
-   P ch_W → P ch_X → P ch_Y → P ch_Z → P ch_a → P ch_b → P ch_c → P ch_d → P ch_e → P ch_f → P ch_g →
-   P ch_h → P ch_i → P ch_j → P ch_k → P ch_l → P ch_m → P ch_n → P ch_o → P ch_p → P ch_q → P ch_r →
-   P ch_s → P ch_t → P ch_u → P ch_v → P ch_w → P ch_x → P ch_y → P ch_z → Πa:ascii.P a ≝
-λP:ascii → Set.
-λp:P ch_0.λp1:P ch_1.λp2:P ch_2.λp3:P ch_3.λp4:P ch_4.λp5:P ch_5.λp6:P ch_6.λp7:P ch_7.λp8:P ch_8.λp9:P ch_9.
-λp10:P ch__.λp11:P ch_A.λp12:P ch_B.λp13:P ch_C.λp14:P ch_D.λp15:P ch_E.λp16:P ch_F.λp17:P ch_G.λp18:P ch_H.
-λp19:P ch_I.λp20:P ch_J.λp21:P ch_K.λp22:P ch_L.λp23:P ch_M.λp24:P ch_N.λp25:P ch_O.λp26:P ch_P.λp27:P ch_Q.
-λp28:P ch_R.λp29:P ch_S.λp30:P ch_T.λp31:P ch_U.λp32:P ch_V.λp33:P ch_W.λp34:P ch_X.λp35:P ch_Y.λp36:P ch_Z.
-λp37:P ch_a.λp38:P ch_b.λp39:P ch_c.λp40:P ch_d.λp41:P ch_e.λp42:P ch_f.λp43:P ch_g.λp44:P ch_h.λp45:P ch_i.
-λp46:P ch_j.λp47:P ch_k.λp48:P ch_l.λp49:P ch_m.λp50:P ch_n.λp51:P ch_o.λp52:P ch_p.λp53:P ch_q.λp54:P ch_r.
-λp55:P ch_s.λp56:P ch_t.λp57:P ch_u.λp58:P ch_v.λp59:P ch_w.λp60:P ch_x.λp61:P ch_y.λp62:P ch_z.λa:ascii.
- match a with
-  [ ch_0 ⇒ p | ch_1 ⇒ p1 | ch_2 ⇒ p2 | ch_3 ⇒ p3 | ch_4 ⇒ p4 | ch_5 ⇒ p5 | ch_6 ⇒ p6 | ch_7 ⇒ p7
-  | ch_8 ⇒ p8 | ch_9 ⇒ p9 | ch__ ⇒ p10 | ch_A ⇒ p11 | ch_B ⇒ p12 | ch_C ⇒ p13 | ch_D ⇒ p14 | ch_E ⇒ p15
-  | ch_F ⇒ p16 | ch_G ⇒ p17 | ch_H ⇒ p18 | ch_I ⇒ p19 | ch_J ⇒ p20 | ch_K ⇒ p21 | ch_L ⇒ p22 | ch_M ⇒ p23
-  | ch_N ⇒ p24 | ch_O ⇒ p25 | ch_P ⇒ p26 | ch_Q ⇒ p27 | ch_R ⇒ p28 | ch_S ⇒ p29 | ch_T ⇒ p30 | ch_U ⇒ p31
-  | ch_V ⇒ p32 | ch_W ⇒ p33 | ch_X ⇒ p34 | ch_Y ⇒ p35 | ch_Z ⇒ p36 | ch_a ⇒ p37 | ch_b ⇒ p38 | ch_c ⇒ p39
-  | ch_d ⇒ p40 | ch_e ⇒ p41 | ch_f ⇒ p42 | ch_g ⇒ p43 | ch_h ⇒ p44 | ch_i ⇒ p45 | ch_j ⇒ p46 | ch_k ⇒ p47
-  | ch_l ⇒ p48 | ch_m ⇒ p49 | ch_n ⇒ p50 | ch_o ⇒ p51 | ch_p ⇒ p52 | ch_q ⇒ p53 | ch_r ⇒ p54 | ch_s ⇒ p55
-  | ch_t ⇒ p56 | ch_u ⇒ p57 | ch_v ⇒ p58 | ch_w ⇒ p59 | ch_x ⇒ p60 | ch_y ⇒ p61 | ch_z ⇒ p62 ].
-
 ndefinition ascii_rect
  : ΠP:ascii → Type.
    P ch_0 → P ch_1 → P ch_2 → P ch_3 → P ch_4 → P ch_5 → P ch_6 → P ch_7 → P ch_8 → P ch_9 → P ch__ →
diff --git a/helm/software/matita/contribs/ng_assembly/utility/ascii_lemmas1.ma b/helm/software/matita/contribs/ng_assembly/utility/ascii_lemmas1.ma
index 4c371c1be..efab13f9d 100755
--- a/helm/software/matita/contribs/ng_assembly/utility/ascii_lemmas1.ma
+++ b/helm/software/matita/contribs/ng_assembly/utility/ascii_lemmas1.ma
@@ -30,7 +30,7 @@ include "freescale/theory.ma".
 ndefinition ascii_destruct1 : Πc2.ΠP:Prop.ch_0 = c2 → match c2 with [ ch_0 ⇒ P → P | _ ⇒ P ].
  #c2; #P; ncases c2; nnormalize;
  ##[ ##1: #H; napply (λx:P.x)
- ##| ##*: #H; napply (False_ind ??); nchange with (match ch_0 with [ ch_0 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
+ ##| ##*: #H; napply (False_ind (λ_.?) ?); nchange with (match ch_0 with [ ch_0 ⇒ False | _ ⇒ True ]); nrewrite > H; nnormalize; napply I
  ##]
 nqed.
 
diff --git a/helm/software/matita/contribs/ng_assembly/utility/string.ma b/helm/software/matita/contribs/ng_assembly/utility/string.ma
index d2a552901..ea1c1ccd1 100644
--- a/helm/software/matita/contribs/ng_assembly/utility/string.ma
+++ b/helm/software/matita/contribs/ng_assembly/utility/string.ma
@@ -51,7 +51,7 @@ nlet rec eq_str (str,str':aux_str_type) ≝
 ninductive aux_strId_type : Type ≝
  STR_ID: aux_str_type → nat → aux_strId_type.
 
-ndefinition aux_strId_type_ind : ΠP:aux_strId_type → Prop.(Πl,n.P (STR_ID l n)) → Πa:aux_strId_type.P a ≝
+(*ndefinition aux_strId_type_ind : ΠP:aux_strId_type → Prop.(Πl,n.P (STR_ID l n)) → Πa:aux_strId_type.P a ≝
 λP:aux_strId_type → Prop.λf:Πl,n.P (STR_ID l n).λa:aux_strId_type.
  match a with [ STR_ID l n ⇒ f l n ].
 
@@ -61,7 +61,7 @@ ndefinition aux_strId_type_rec : ΠP:aux_strId_type → Set.(Πl,n.P (STR_ID l n
 
 ndefinition aux_strId_type_rect : ΠP:aux_strId_type → Type.(Πl,n.P (STR_ID l n)) → Πa:aux_strId_type.P a ≝
 λP:aux_strId_type → Type.λf:Πl,n.P (STR_ID l n).λa:aux_strId_type.
- match a with [ STR_ID l n ⇒ f l n ].
+ match a with [ STR_ID l n ⇒ f l n ].*)
 
 (* getter *)
 ndefinition get_name_strId ≝ λsid:aux_strId_type.match sid with [ STR_ID n _ ⇒ n ].
diff --git a/helm/software/matita/contribs/ng_assembly/utility/utility.ma b/helm/software/matita/contribs/ng_assembly/utility/utility.ma
index 2f8362b37..69d88e8cb 100755
--- a/helm/software/matita/contribs/ng_assembly/utility/utility.ma
+++ b/helm/software/matita/contribs/ng_assembly/utility/utility.ma
@@ -33,14 +33,14 @@ ninductive ne_list (A:Type) : Type ≝
   | ne_nil: A → ne_list A
   | ne_cons: A → ne_list A → ne_list A.
 
-nlet rec ne_list_ind (A:Type) (P:ne_list A → Prop) (f:Πd.P (ne_nil A d)) (f1:(Πa:A.Πl':ne_list A.P l' → P (ne_cons A a l'))) (l:ne_list A) on l ≝
+(*nlet rec ne_list_ind (A:Type) (P:ne_list A → Prop) (f:Πd.P (ne_nil A d)) (f1:(Πa:A.Πl':ne_list A.P l' → P (ne_cons A a l'))) (l:ne_list A) on l ≝
  match l with [ ne_nil d ⇒ f d | ne_cons h t ⇒ f1 h t (ne_list_ind A P f f1 t) ].
 
 nlet rec ne_list_rec (A:Type) (P:ne_list A → Set) (f:Πd.P (ne_nil A d)) (f1:(Πa:A.Πl':ne_list A.P l' → P (ne_cons A a l'))) (l:ne_list A) on l ≝
  match l with [ ne_nil d ⇒ f d | ne_cons h t ⇒ f1 h t (ne_list_rec A P f f1 t) ].
 
 nlet rec ne_list_rect (A:Type) (P:ne_list A → Type) (f:Πd.P (ne_nil A d)) (f1:(Πa:A.Πl':ne_list A.P l' → P (ne_cons A a l'))) (l:ne_list A) on l ≝
- match l with [ ne_nil d ⇒ f d | ne_cons h t ⇒ f1 h t (ne_list_rect A P f f1 t) ].
+ match l with [ ne_nil d ⇒ f d | ne_cons h t ⇒ f1 h t (ne_list_rect A P f f1 t) ].*)
 
 (* append *)
 nlet rec ne_append (A:Type) (l1,l2:ne_list A) on l1 ≝
@@ -104,7 +104,7 @@ ndefinition list_to_neList ≝
  match l
   return λl:list T.isnot_empty_list T l → ne_list T
  with
-  [ nil ⇒ λp:isnot_empty_list T (nil T).False_rect ? p
+  [ nil ⇒ λp:isnot_empty_list T (nil T).False_rect_Type0 ? p
   | cons h t ⇒ λp:isnot_empty_list T (cons T h t).
    match list_to_neList_aux T t with
     [ None ⇒ «£h»
@@ -260,11 +260,11 @@ nlet rec fold_right_list2 (T1,T2:Type) (f:T1 → T1 → T2 → T2) (acc:T2) (l1:
   [ nil ⇒ λl2.match l2 return λl2.len_list T1 [] = len_list T1 l2 → T2 with
    [ nil ⇒ λp:len_list T1 [] = len_list T1 [].acc
    | cons h t ⇒ λp:len_list T1 [] = len_list T1 (h::t).
-    False_rect ? (fold_right_list2_aux1 T1 h t p)
+    False_rect_Type0 ? (fold_right_list2_aux1 T1 h t p)
    ]
   | cons h t ⇒ λl2.match l2 return λl2.len_list T1 (h::t) = len_list T1 l2 → T2 with
    [ nil ⇒ λp:len_list T1 (h::t) = len_list T1 [].
-    False_rect ? (fold_right_list2_aux2 T1 h t p)
+    False_rect_Type0 ? (fold_right_list2_aux2 T1 h t p)
    | cons h' t' ⇒ λp:len_list T1 (h::t) = len_list T1 (h'::t').
     f h h' (fold_right_list2 T1 T2 f acc t t' (fold_right_list2_aux3 T1 h h' t t' p))
    ]
@@ -321,11 +321,11 @@ nlet rec fold_right_neList2 (T1,T2:Type) (f:T1 → T1 → T2 → T2) (acc:T2) (l
    [ ne_nil h' ⇒ λp:len_neList T1 «£h» = len_neList T1 «£h'».
     f h h' acc
    | ne_cons h' t' ⇒ λp:len_neList T1 «£h» = len_neList T1 (h'§§t').
-    False_rect ? (fold_right_neList2_aux1 T1 h h' t' p)
+    False_rect_Type0 ? (fold_right_neList2_aux1 T1 h h' t' p)
    ]
   | ne_cons h t ⇒ λl2.match l2 return λl2.len_neList T1 (h§§t) = len_neList T1 l2 → T2 with
    [ ne_nil h' ⇒ λp:len_neList T1 (h§§t) = len_neList T1 «£h'».
-    False_rect ? (fold_right_neList2_aux2 T1 h h' t p)
+    False_rect_Type0 ? (fold_right_neList2_aux2 T1 h h' t p)
    | ne_cons h' t' ⇒ λp:len_neList T1 (h§§t) = len_neList T1 (h'§§t').
     f h h' (fold_right_neList2 T1 T2 f acc t t' (fold_right_neList2_aux3 T1 h h' t t' p))
    ]