]> matita.cs.unibo.it Git - helm.git/commitdiff
set -> type
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 10 Apr 2007 14:32:28 +0000 (14:32 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 10 Apr 2007 14:32:28 +0000 (14:32 +0000)
matita/library/Fsub/defn.ma
matita/library/Fsub/part1a.ma
matita/library/Fsub/util.ma
matita/library/list/sort.ma
matita/tests/discriminate.ma

index 8ff30ce1f7411f5424506ff6f011fbd75584fe23..97e161967e86f1923e88cfad37a78f55317b887c 100644 (file)
@@ -21,7 +21,7 @@ include "list/list.ma".
 include "Fsub/util.ma".
 
 (*** representation of Fsub types ***)  
-inductive Typ : Set \def
+inductive Typ : Type \def
   | TVar : nat \to Typ            (* type var *)
   | TFree: nat \to Typ            (* free type name *)
   | Top : Typ                     (* maximum type *)
@@ -29,7 +29,7 @@ inductive Typ : Set \def
   | Forall : Typ \to Typ \to Typ. (* universal type *)
   
 (*** representation of Fsub terms ***)
-inductive Term : Set \def
+inductive Term : Type \def
   | Var : nat \to Term            (* variable *)
   | Free : nat \to Term          (* free name *)
   | Abs : Typ \to Term \to Term   (* abstraction *)
@@ -39,7 +39,7 @@ inductive Term : Set \def
   
 (* representation of bounds *)
 
-record bound : Set \def { 
+record bound : Type \def { 
                           istype : bool;    (* is subtyping bound? *)
                           name   : nat ;    (* name *)
                           btype  : Typ      (* type to which the name is bound *)
@@ -354,11 +354,11 @@ lemma natinfv_boundinenv : \forall x,G.(in_list ? x (fv_env G)) \to
                               \exists B,T.(in_list ? (mk_bound B x T) G).
 intros 2;elim G 0
   [simplify;intro;lapply (in_list_nil ? ? H);elim Hletin
-  |intros 3;elim s;simplify in H1;inversion H1
+  |intros 3;elim t;simplify in H1;inversion H1
      [intros;rewrite < H2;simplify;apply ex_intro
         [apply b
         |apply ex_intro
-           [apply t
+           [apply t1
            |lapply (inj_head_nat ? ? ? ? H3);rewrite > H2;rewrite < Hletin;
             apply in_Base]]
      |intros;lapply (inj_tail ? ? ? ? ? H5);rewrite < Hletin in H2;
@@ -411,7 +411,7 @@ lemma varin_envappend_case: \forall G,H,x.(var_in_env x (H @ G)) \to
                             (var_in_env x G) \lor (var_in_env x H).
 intros 3.elim H 0
   [simplify;intro;left;assumption
-  |intros 2;elim s;simplify in H2;inversion H2
+  |intros 2;elim t;simplify in H2;inversion H2
      [intros;lapply (inj_head_nat ? ? ? ? H4);rewrite > Hletin;right;
       simplify;constructor 1
      |intros;lapply (inj_tail ? ? ? ? ? H6);
@@ -441,10 +441,10 @@ lemma varinG_or_varinH_to_varinGH : \forall G,H,x.
 intros.elim H1 0
   [elim H
      [simplify;assumption
-     |elim s;simplify;constructor 2;apply (H2 H3)]
+     |elim t;simplify;constructor 2;apply (H2 H3)]
   |elim H 0
      [simplify;intro;lapply (in_list_nil nat x H2);elim Hletin
-     |intros 2;elim s;simplify in H3;inversion H3
+     |intros 2;elim t;simplify in H3;inversion H3
         [intros;lapply (inj_head_nat ? ? ? ? H5);rewrite > Hletin;simplify;
          constructor 1
         |intros;simplify;constructor 2;rewrite < H6;apply H2;
@@ -481,7 +481,7 @@ lemma fv_env_extends : \forall H,x,B,C,T,U,G.
                           (fv_env (H @ ((mk_bound C x U) :: G))).
 intros;elim H
   [simplify;reflexivity
-  |elim s;simplify;rewrite > H1;reflexivity]
+  |elim t;simplify;rewrite > H1;reflexivity]
 qed.
 
 lemma lookup_env_extends : \forall G,H,B,C,D,T,U,V,x,y.
@@ -597,7 +597,7 @@ lemma lookup_swap : \forall x,u,v,T,B,G.(in_list ? (mk_bound B x T) G) \to
     (in_list ? (mk_bound B (swap u v x) (swap_Typ u v T)) (swap_Env u v G)).
 intros 6;elim G 0
   [intros;elim (in_list_nil ? ? H)
-  |intro;elim s;simplify;inversion H1
+  |intro;elim t;simplify;inversion H1
      [intros;lapply (inj_head ? ? ? ? H3);rewrite < H2 in Hletin;
       destruct Hletin;rewrite > Hcut;rewrite > Hcut1;rewrite > Hcut2;
       apply in_Base
@@ -628,13 +628,13 @@ lemma in_dom_swap : \forall u,v,x,G.
 intros;split
   [elim G 0
      [simplify;intro;elim (in_list_nil ? ? H)
-     |intro;elim s 0;simplify;intros;inversion H1
+     |intro;elim t 0;simplify;intros;inversion H1
         [intros;lapply (inj_head_nat ? ? ? ? H3);rewrite > Hletin;apply in_Base
         |intros;lapply (inj_tail ? ? ? ? ? H5);rewrite < Hletin in H2;
          rewrite > H4 in H;apply in_Skip;apply (H H2)]]
   |elim G 0
      [simplify;intro;elim (in_list_nil ? ? H)
-     |intro;elim s 0;simplify;intros;inversion H1
+     |intro;elim t 0;simplify;intros;inversion H1
         [intros;lapply (inj_head_nat ? ? ? ? H3);rewrite < H2 in Hletin;
          lapply (swap_inj ? ? ? ? Hletin);rewrite > Hletin1;apply in_Base
         |intros;lapply (inj_tail ? ? ? ? ? H5);rewrite < Hletin in H2;
@@ -657,7 +657,7 @@ cut (\forall l:(list nat).\exists n.\forall m.
              [assumption|apply nil_cons]
           |intros;lapply (sym_eq ? ? ? H5);absurd (a1::l1 = [])
              [assumption|apply nil_cons]]]
-    |elim H;lapply (decidable_eq_nat a s);elim Hletin
+    |elim H;lapply (decidable_eq_nat a t);elim Hletin
        [apply ex_intro
           [apply (S a)
           |intros;unfold;intro;inversion H4
@@ -668,23 +668,23 @@ cut (\forall l:(list nat).\exists n.\forall m.
               rewrite < H7 in H5;
               apply (H1 m ? H5);lapply (le_S ? ? H3);
               apply (le_S_S_to_le ? ? Hletin2)]]
-       |cut ((leb a s) = true \lor (leb a s) = false)
+       |cut ((leb a t) = true \lor (leb a t) = false)
           [elim Hcut
              [apply ex_intro
-                [apply (S s)
+                [apply (S t)
                 |intros;unfold;intro;inversion H5
                    [intros;lapply (inj_head_nat ? ? ? ? H7);rewrite > H6 in H4;
                     rewrite < Hletin1 in H4;apply (not_le_Sn_n ? H4)
                    |intros;lapply (inj_tail ? ? ? ? ? H9);
                     rewrite < Hletin1 in H6;lapply (H1 a1)
                       [apply (Hletin2 H6)
-                      |lapply (leb_to_Prop a s);rewrite > H3 in Hletin2;
+                      |lapply (leb_to_Prop a t);rewrite > H3 in Hletin2;
                        simplify in Hletin2;rewrite < H8;
                        apply (trans_le ? ? ? Hletin2);
                        apply (trans_le ? ? ? ? H4);constructor 2;constructor 1]]]
              |apply ex_intro
                 [apply a
-                |intros;lapply (leb_to_Prop a s);rewrite > H3 in Hletin1;
+                |intros;lapply (leb_to_Prop a t);rewrite > H3 in Hletin1;
                  simplify in Hletin1;lapply (not_le_to_lt ? ? Hletin1);
                  unfold in Hletin2;unfold;intro;inversion H5
                    [intros;lapply (inj_head_nat ? ? ? ? H7);
@@ -693,7 +693,7 @@ cut (\forall l:(list nat).\exists n.\forall m.
                    |intros;lapply (inj_tail ? ? ? ? ? H9);
                     rewrite < Hletin3 in H6;rewrite < H8 in H6;
                     apply (H1 ? H4 H6)]]]
-          |elim (leb a s);auto]]]]
+          |elim (leb a t);auto]]]]
 qed.
 
 (*** lemmas on well-formedness ***)
@@ -794,17 +794,17 @@ qed.
 lemma WFE_swap : \forall u,v,G.(WFEnv G) \to (WFEnv (swap_Env u v G)).
 intros 3.elim G 0
   [intro;simplify;assumption
-  |intros 2;elim s;simplify;constructor 2
+  |intros 2;elim t;simplify;constructor 2
      [apply H;apply (WFE_consG_WFE_G ? ? H1)
      |unfold;intro;lapply (in_dom_swap u v n l);elim Hletin;lapply (H4 H2);
       (* FIXME trick *)generalize in match H1;intro;inversion H1
-        [intros;absurd ((mk_bound b n t)::l = [])
+        [intros;absurd ((mk_bound b n t1)::l = [])
            [assumption|apply nil_cons]
         |intros;lapply (inj_head ? ? ? ? H10);lapply (inj_tail ? ? ? ? ? H10);
          destruct Hletin2;rewrite < Hcut1 in H8;rewrite < Hletin3 in H8;
          apply (H8 Hletin1)]
-     |apply (WFT_swap u v l t);inversion H1
-        [intro;absurd ((mk_bound b n t)::l = [])
+     |apply (WFT_swap u v l t1);inversion H1
+        [intro;absurd ((mk_bound b n t1)::l = [])
            [assumption|apply nil_cons]
         |intros;lapply (inj_head ? ? ? ? H6);lapply (inj_tail ? ? ? ? ? H6);
          destruct Hletin;rewrite > Hletin1;rewrite > Hcut2;assumption]]]
@@ -929,11 +929,11 @@ lemma swap_env_not_free : \forall u,v,G.(WFEnv G) \to
                                         (swap_Env u v G) = G.
 intros 3.elim G 0
   [simplify;intros;reflexivity
-  |intros 2;elim s 0;simplify;intros;lapply (notin_cons ? ? ? ? H2);
+  |intros 2;elim t 0;simplify;intros;lapply (notin_cons ? ? ? ? H2);
    lapply (notin_cons ? ? ? ? H3);elim Hletin;elim Hletin1;
    lapply (swap_other ? ? ? H4 H6);lapply (WFE_consG_to_WFT ? ? ? ? H1);
-   cut (\lnot (in_list ? u (fv_type t)))
-     [cut (\lnot (in_list ? v (fv_type t)))
+   cut (\lnot (in_list ? u (fv_type t1)))
+     [cut (\lnot (in_list ? v (fv_type t1)))
         [lapply (swap_Typ_not_free ? ? ? Hcut Hcut1);
          lapply (WFE_consG_WFE_G ? ? H1);
          lapply (H Hletin5 H5 H7);
@@ -1123,9 +1123,9 @@ intros 7;elim H 0
      |intros;lapply (inj_tail ? ? ? ? ? H8);lapply (inj_head ? ? ? ? H8);
       destruct Hletin1;rewrite < Hletin in H6;rewrite < Hletin in H4;
       rewrite < Hcut1 in H6;apply (WFE_cons ? ? ? ? H4 H6 H2)]
-  |intros;simplify;generalize in match H2;elim s;simplify in H4;
+  |intros;simplify;generalize in match H2;elim t;simplify in H4;
    inversion H4
-     [intros;absurd (mk_bound b n t::l@(mk_bound B x T::G)=Empty)
+     [intros;absurd (mk_bound b n t1::l@(mk_bound B x T::G)=Empty)
         [assumption
         |apply nil_cons]
      |intros;lapply (inj_tail ? ? ? ? ? H9);lapply (inj_head ? ? ? ? H9);
index e12a64be4809093d647ba9f04a8906d42d2a9f83..795546299e842f8c2f2824a7c102db04e548d5d1 100644 (file)
@@ -176,7 +176,7 @@ cut (\forall G,T,Q.(JSubtype G T Q) \to
                  |simplify;apply incl_nat_cons;assumption]]]
         |elim G2 0
            [simplify;unfold;intros;assumption
-           |intro;elim s 0;simplify;intros;apply incl_nat_cons;assumption]]]
+           |intro;elim t 0;simplify;intros;apply incl_nat_cons;assumption]]]
   |intros 4;(*generalize in match H1;*)elim H1
      [inversion H5
         [intros;rewrite < H8;apply (SA_Top ? ? H2 H3)
index 8b111e3f2425637f1fc75086a96265cb78ff6db7..582114c690a60afb840fa51b0eaaac2801c899ea 100644 (file)
@@ -35,7 +35,7 @@ let rec max m n \def
      [true \Rightarrow n
      |false \Rightarrow m]. 
 
-inductive in_list (A : Set) : A \to (list A) \to Prop \def
+inductive in_list (A : Type) : A \to (list A) \to Prop \def
   | in_Base : \forall x:A.\forall l:(list A).
               (in_list A x (x :: l))
   | in_Skip : \forall x,y:A.\forall l:(list A).
index 939cecedec6486a27274a4ce6ac834888f7c58ce..d182ed6d68bd1148b663a3d494cd18baf996d306 100644 (file)
@@ -18,7 +18,7 @@ include "datatypes/bool.ma".
 include "datatypes/constructors.ma".
 include "list/list.ma".
 
-let rec mem (A:Set) (eq: A → A → bool) x (l: list A) on l ≝
+let rec mem (A:Type) (eq: A → A → bool) x (l: list A) on l ≝
  match l with
   [ nil ⇒ false
   | (cons a l') ⇒
@@ -28,7 +28,7 @@ let rec mem (A:Set) (eq: A → A → bool) x (l: list A) on l ≝
      ]
   ].
   
-let rec ordered (A:Set) (le: A → A → bool) (l: list A) on l ≝
+let rec ordered (A:Type) (le: A → A → bool) (l: list A) on l ≝
  match l with
   [ nil ⇒ true
   | (cons x l') ⇒
@@ -39,7 +39,7 @@ let rec ordered (A:Set) (le: A → A → bool) (l: list A) on l ≝
       ]
   ].
   
-let rec insert (A:Set) (le: A → A → bool) x (l: list A) on l ≝
+let rec insert (A:Type) (le: A → A → bool) x (l: list A) on l ≝
  match l with
   [ nil ⇒ [x]
   | (cons he l') ⇒
@@ -50,7 +50,7 @@ let rec insert (A:Set) (le: A → A → bool) x (l: list A) on l ≝
   ].
 
 lemma insert_ind :
- ∀A:Set. ∀le: A → A → bool. ∀x.
+ ∀A:Type. ∀le: A → A → bool. ∀x.
   ∀P:(list A → list A → Prop).
    ∀H:(∀l: list A. l=[] → P [] [x]).
     ∀H2:
@@ -86,7 +86,7 @@ lemma insert_ind :
 qed.
 
 
-let rec insertionsort (A:Set) (le: A → A → bool) (l: list A) on l ≝
+let rec insertionsort (A:Type) (le: A → A → bool) (l: list A) on l ≝
  match l with
   [ nil ⇒ []
   | (cons he l') ⇒
@@ -95,7 +95,7 @@ let rec insertionsort (A:Set) (le: A → A → bool) (l: list A) on l ≝
   ].
 
 lemma ordered_injective:
-  ∀A:Set. ∀le:A → A → bool.
+  ∀A:Type. ∀le:A → A → bool.
    ∀l:list A. ordered A le l = true → ordered A le (tail A l) = true.
   intros 3 (A le l).
   elim l
@@ -105,12 +105,12 @@ lemma ordered_injective:
     clear H1;
     elim l1;
     [ simplify; reflexivity;
-    | cut ((le s s1 \land ordered A le (s1::l2)) = true);
+    | cut ((le t t1 \land ordered A le (t1::l2)) = true);
       [ generalize in match Hcut; 
         apply andb_elim;
-        elim (le s s1);
+        elim (le t t1);
         [ simplify;
-          fold simplify (ordered ? le (s1::l2));
+          fold simplify (ordered ? le (t1::l2));
           intros; assumption;
         | simplify;
           intros (Habsurd);
@@ -126,7 +126,7 @@ lemma ordered_injective:
 qed.
 
 lemma insert_sorted:
-  \forall A:Set. \forall le:A\to A\to bool.
+  \forall A:Type. \forall le:A\to A\to bool.
   (\forall a,b:A. le a b = false \to le b a = true) \to
   \forall l:list A. \forall x:A.
     ordered A le l = true \to ordered A le (insert A le x l) = true.
@@ -139,7 +139,7 @@ lemma insert_sorted:
       elim l'; simplify;
       [ rewrite > H5;
         reflexivity
-      | elim (le x s); simplify;
+      | elim (le x t); simplify;
         [ rewrite > H5;
           reflexivity
         | simplify in H4;
@@ -157,7 +157,7 @@ lemma insert_sorted:
 qed.
   
 theorem insertionsort_sorted:
-  ∀A:Set.
+  ∀A:Type.
   ∀le:A → A → bool.∀eq:A → A → bool.
   (∀a,b:A. le a b = false → le b a = true) \to
   ∀l:list A.
@@ -166,7 +166,7 @@ theorem insertionsort_sorted:
   elim l;
   [ simplify;
     reflexivity;
-  | apply (insert_sorted ? ? le_tot (insertionsort ? le l1) s);
+  | apply (insert_sorted ? ? le_tot (insertionsort ? le l1) t);
     assumption;
   ]
 qed.
\ No newline at end of file
index 81c2da87fbf381b9d8954088a41ee9ce44c465cb..b1d7b9ca68a74ef5b96959ee19e4ccbe2031cee5 100644 (file)
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/tests/discriminate".
-include "../legacy/coq.ma".
-alias id "not" = "cic:/Coq/Init/Logic/not.con".
-alias num (instance 0) = "natural number".
-alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
-alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)".
-alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)".
-alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
-alias id "bool" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1)".
-alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
-alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
-
-inductive foo: Prop \def I_foo: foo.
-
-alias num (instance 0) = "binary integer number".
+
+include "logic/equality.ma".
+include "nat/nat.ma".
+include "datatypes/constructors.ma".
+
 theorem stupid:
-  1 = 0 \to (\forall p:Prop. p \to not p).
+  (S O) = O \to (\forall p:Prop. p \to Not p).
   intros.
-  generalize in match I_foo.
+  generalize in match I.
   destruct H.
 qed.
 
@@ -38,7 +29,6 @@ inductive bar_list (A:Set): Set \def
   | bar_nil: bar_list A
   | bar_cons: A \to bar_list A \to bar_list A.
 
-
 theorem stupid2:
   \forall A:Set.\forall x:A.\forall l:bar_list A.
   bar_nil A = bar_cons A x l \to False.
@@ -69,3 +59,64 @@ theorem recursive: S (S (S O)) = S (S O) \to False.
  intros;
  destruct H.
 qed.
+
+inductive complex (A,B : Type) : B → A → Type ≝
+| C1 : ∀x:nat.∀a:A.∀b:B. complex A B b a
+| C2 : ∀a,a1:A.∀b,b1:B.∀x:nat. complex A B b1 a1 → complex A B b a.
+
+
+theorem recursive1: ∀ x,y : nat. 
+  (C1 ? ? O     (Some ? x) y) = 
+  (C1 ? ? (S O) (Some ? x) y) → False.
+intros; destruct H;
+qed.
+
+theorem recursive2: ∀ x,y,z,t : nat. 
+  (C1 ? ? t (Some ? x) y) = 
+  (C1 ? ? z (Some ? x) y) → t=z.
+intros; destruct H;assumption.
+qed.
+
+theorem recursive3: ∀ x,y,z,t : nat. 
+  C2 ? ? (None ?) ? (S O) ? z (C1 ? ? (S O) (Some ? x) y) = 
+  C2 ? ? (None ?) ? (S O) ? t (C1 ? ? (S O) (Some ? x) y) → z=t.
+intros; destruct H;assumption.
+qed.
+
+theorem recursive4: ∀ x,y,z,t : nat. 
+  C2 ? ? (None ?) ? (S O) ? z (C1 ? ? (S O) (Some ? z) y) = 
+  C2 ? ? (None ?) ? (S O) ? t (C1 ? ? (S O) (Some ? x) y) → z=t.
+intros; 
+
+
+
+
+ (λHH  : ((C1 (option nat) nat (S O) (Some nat -7) -8) = (C1 (option nat) nat (S O) (Some nat -9) -8))
+  eq_elim_r 
+    (complex (option nat) nat -8 (Some nat -7)) 
+    (C1 (option nat) nat (S O) (Some nat -9) -8) 
+    (λc:(complex (option nat) nat -8 (Some nat -7)).
+      (eq (option nat) 
+        ((λx:(complex (option nat) nat -8 (Some nat -7)).
+           match x return (λy1:nat.(λy2:(option nat).(λ x:(complex (option nat) nat y1 y2).(option nat)))) with
+           [ (C1 (y1:nat) (a:(option nat)) (b:nat)) => a
+           | (C2 (a:(option nat)) (a1:(option nat)) (b:nat) (b1:nat) (y2:nat) (y3:(complex (option nat) nat b1 a1))) ⇒
+              (Some nat -7)
+           ]) c) 
+        (Some nat -9))) 
+     ? 
+     (C1 (option nat) nat (S O) (Some nat -7) -8) 
+     HH)
+
+
+
+
+destruct H;assumption.
+qed.
+
+theorem recursive2: ∀ x,y : nat. 
+  C2 ? ? (None ?) ? (S O) ? O (C1 ? ? O     (Some ? x) y) = 
+  C2 ? ? (None ?) ? (S O) ? O (C1 ? ? (S O) (Some ? x) y) → False.
+intros; destruct H;
+
+