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 *)
| 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 *)
(* 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 *)
\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;
(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);
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;
(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.
(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
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;
[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
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);
|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 ***)
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]]]
(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);
|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);
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') ⇒
]
].
-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') ⇒
]
].
-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') ⇒
].
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:
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') ⇒
].
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
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);
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.
elim l'; simplify;
[ rewrite > H5;
reflexivity
- | elim (le x s); simplify;
+ | elim (le x t); simplify;
[ rewrite > H5;
reflexivity
| simplify in H4;
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.
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
(**************************************************************************)
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.
| 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.
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;
+
+
projects / helm.git / commitdiff