∀T1,T2:Type[0].∀l1:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 T1.∀l2:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 T2.∀P:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 T1 → \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 T2 → Prop.
\ 5a href="cic:/matita/basics/list/length.fix(0,1,1)"\ 6length\ 5/a\ 6 ? l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/list/length.fix(0,1,1)"\ 6length\ 5/a\ 6 ? l2 →
(P (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 ?) (\ 5a href="cic:/matita/basics/list/list.con(0,1,1)"\ 6nil\ 5/a\ 6 ?)) →
- (∀hd1,hd2,tl1,tl2. P tl1 tl2 → P (hd1\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:tl1) (hd2\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:tl2)) →
+ (∀hd1,hd2,tl1,tl2. P tl1 tl2 → P (hd1\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6tl1) (hd2\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6tl2)) →
P l1 l2.
#T1 #T2 #l1 #l2 #P #Hl #Pnil #Pcons
generalize in match Hl; generalize in match l2;
qed.
inductive in_list (A:Type[0]): A → (\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) → Prop ≝
-| in_list_head : ∀ x,l.(in_list A x (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l))
-| in_list_cons : ∀ x,y,l.(in_list A x l) → (in_list A x (y\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l)).
+| in_list_head : ∀ x,l.(in_list A x (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l))
+| in_list_cons : ∀ x,y,l.(in_list A x l) → (in_list A x (y\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l)).
definition incl : ∀A.(\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) → (\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) → Prop ≝
λA,l,m.∀x.\ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 A x l → \ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 A x m.
interpretation "list not member" 'notmem x l = (Not (in_list ? x l)).
interpretation "list inclusion" 'subseteq l1 l2 = (incl ? l1 l2).
-axiom not_in_list_nil : ∀A,x.\ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 A x \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6].
+axiom not_in_list_nil : ∀A,x.\ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 A x [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6.
(*intros.unfold.intro.inversion H
[intros;lapply (sym_eq ? ? ? H2);destruct Hletin
|intros;destruct H4]
qed.*)
-axiom in_list_cons_case : ∀A,x,a,l.\ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 A x (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l) →
+axiom in_list_cons_case : ∀A,x,a,l.\ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 A x (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l) →
x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 A x l.
(*intros;inversion H;intros
[destruct H2;left;reflexivity
qed.*)
axiom in_list_tail : ∀l,x,y.
- \ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 x (y\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l) → x \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 y → \ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 x l.
+ \ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 x (y\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6l) → x \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 y → \ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 x l.
(*intros 4;elim (in_list_cons_case ? ? ? ? H)
[elim (H2 H1)
|assumption]
qed.*)
-axiom in_list_singleton_to_eq : ∀A,x,y.\ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 A x (y\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]) → x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 y.
+axiom in_list_singleton_to_eq : ∀A,x,y.\ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 A x \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6y\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 → x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 y.
(*intros;elim (in_list_cons_case ? ? ? ? H)
[assumption
|elim (not_in_list_nil ? ? H1)]
]
qed.
+lemma bool_elim :
+∀P:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → Prop.∀b.(b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → P \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6) → (b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 → P \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6) → P b.
+#P * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
+qed.
-(*
-let rec mem (A:Type) (eq: A → A → bool) x (l: list A) on l ≝
+let rec mem (A:Type[0]) (eq: A → A → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6) x (l: \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A) on l ≝
match l with
- [ nil ⇒ false
+ [ nil ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6
| (cons a l') ⇒
match eq x a with
- [ true ⇒ true
+ [ true ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6
| false ⇒ mem A eq x l'
]
].
-naxiom mem_true_to_in_list :
- \forall A,equ.
- (\forall x,y.equ x y = true \to x = y) \to
- \forall x,l.mem A equ x l = true \to in_list A x l.
+axiom mem_true_to_in_list :
+ ∀A,equ.
+ (∀x,y.equ x y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 y) →
+ ∀x,l.\ 5a href="cic:/matita/cr/lambda/mem.fix(0,3,1)"\ 6mem\ 5/a\ 6 A equ x l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → \ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 A x l.
(* intros 5.elim l
[simplify in H1;destruct H1
|simplify in H2;apply (bool_elim ? (equ x a))
apply in_list_cons;apply H1;assumption]]
qed.*)
-naxiom in_list_to_mem_true :
- \forall A,equ.
- (\forall x.equ x x = true) \to
- \forall x,l.in_list A x l \to mem A equ x l = true.
+axiom in_list_to_mem_true :
+ ∀A,equ.
+ (∀x.equ x x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6) →
+ ∀x,l.\ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"\ 6in_list\ 5/a\ 6 A x l → \ 5a href="cic:/matita/cr/lambda/mem.fix(0,3,1)"\ 6mem\ 5/a\ 6 A equ x l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
(*intros 5.elim l
[elim (not_in_list_nil ? ? H1)
|elim H2
|simplify;rewrite > H4;apply (bool_elim ? (equ a1 a2));intro;reflexivity]].
qed.*)
-naxiom in_list_filter_to_p_true : \forall A,l,x,p.
-in_list A x (filter A l p) \to p x = true.
+lemma not_in_list_to_mem_false :
+ ∀A,equ. (∀x,y.equ x y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 y) →
+ ∀x,l.x \ 5a title="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 l → \ 5a href="cic:/matita/cr/lambda/mem.fix(0,3,1)"\ 6mem\ 5/a\ 6 A equ x l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6.
+#A #equ #H1 #x #l #H2
+@(\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"\ 6bool_elim\ 5/a\ 6 … (\ 5a href="cic:/matita/cr/lambda/mem.fix(0,3,1)"\ 6mem\ 5/a\ 6 A equ x l)) //
+#H3 cases H2 #H4 cases (H4 ?) @(\ 5a href="cic:/matita/cr/lambda/mem_true_to_in_list.dec"\ 6mem_true_to_in_list\ 5/a\ 6 … H3) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
+qed.
+
+lemma mem_false_to_not_in_list :
+ ∀A,equ. (∀x.equ x x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6) →
+ ∀x,l.\ 5a href="cic:/matita/cr/lambda/mem.fix(0,3,1)"\ 6mem\ 5/a\ 6 A equ x l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 → x \ 5a title="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 l.
+#A #equ #H1 #x #l #H2 % #H3
+>(\ 5a href="cic:/matita/cr/lambda/in_list_to_mem_true.dec"\ 6in_list_to_mem_true\ 5/a\ 6 ????? H3) in H2; /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+qed.
+
+(*
+axiom in_list_filter_to_p_true : ∀A,l,x,p.
+in_list A x (filter A l p) → p x = true.
(* intros 4;elim l
[simplify in H;elim (not_in_list_nil ? ? H)
|simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1;
[apply in_list_cons;apply H;assumption
|apply H;assumption]]]
qed.*)
+*)
-naxiom incl_A_A: ∀T,A.incl T A A.
+axiom incl_A_A: ∀T,A.\ 5a href="cic:/matita/cr/lambda/incl.def(1)"\ 6incl\ 5/a\ 6 T A A.
(*intros.unfold incl.intros.assumption.
qed.*)
-naxiom incl_append_l : ∀T,A,B.incl T A (A @ B).
+axiom incl_append_l : ∀T,A,B.\ 5a href="cic:/matita/cr/lambda/incl.def(1)"\ 6incl\ 5/a\ 6 T A (A \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 B).
(*unfold incl; intros;autobatch.
qed.*)
-naxiom incl_append_r : ∀T,A,B.incl T B (A @ B).
+axiom incl_append_r : ∀T,A,B.\ 5a href="cic:/matita/cr/lambda/incl.def(1)"\ 6incl\ 5/a\ 6 T B (A \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 B).
(*unfold incl; intros;autobatch.
qed.*)
-naxiom incl_cons : ∀T,A,B,x.incl T A B → incl T (x::A) (x::B).
+axiom incl_cons : ∀T,A,B,x.\ 5a href="cic:/matita/cr/lambda/incl.def(1)"\ 6incl\ 5/a\ 6 T A B → \ 5a href="cic:/matita/cr/lambda/incl.def(1)"\ 6incl\ 5/a\ 6 T (x:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6A) (x:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6B).
(*unfold incl; intros;elim (in_list_cons_case ? ? ? ? H1);autobatch.
qed.*)
-*)
-
-
record Nset : Type[1] ≝
{
(* carrier is specified as a coercion: when an object X of type Nset is
p_fresh : ∀l.N_fresh l \ 5a title="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 l
}.
-lemma bool_elim :
-∀P:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → Prop.∀b.(b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → P \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6) → (b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 → P \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6) → P b.
-#P * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
-qed.
-
lemma p_eqb3 : ∀X,x,y.x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 y → \ 5a href="cic:/matita/cr/lambda/N_eqb.fix(0,0,2)"\ 6N_eqb\ 5/a\ 6 X x y \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
#X #x #y @(\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"\ 6bool_elim\ 5/a\ 6 ? (\ 5a href="cic:/matita/cr/lambda/N_eqb.fix(0,0,2)"\ 6N_eqb\ 5/a\ 6 X x y)) //
#H1 cases (\ 5a href="cic:/matita/cr/lambda/p_eqb2.fix(0,0,3)"\ 6p_eqb2\ 5/a\ 6 ??? H1) #H2 #H3 cases (H2 H3)
let rec GV t ≝
match t with
- [ Par x ⇒ x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]
- | Var _ ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]
+ [ Par x ⇒ \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6x\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6
+ | Var _ ⇒ [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6
| App u v ⇒ GV u \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 GV v
| Abs u ⇒ GV u ].
qed.
lemma swap_finite : ∀N,u,v.\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6l.∀x.x \ 5a title="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 l → (\ 5a href="cic:/matita/cr/lambda/swap.def(3)"\ 6swap\ 5/a\ 6 N u v) x \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 x.
-#N #u #v %[@ (u\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:v\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6])]
+#N #u #v %[@ \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6u;v\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6]
#x #H1 @\ 5a href="cic:/matita/cr/lambda/swap_other.def(5)"\ 6swap_other\ 5/a\ 6 % #H2 cases H1 #H3 @H3 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/cr/lambda/in_list.con(0,1,1)"\ 6in_list_head\ 5/a\ 6, \ 5a href="cic:/matita/cr/lambda/in_list.con(0,2,1)"\ 6in_list_cons\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
qed.
qed.
*)
-definition Lam ≝ λx:\ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.λM:\ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6.\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"\ 6Abs\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/vclose.fix(0,0,4)"\ 6vclose\ 5/a\ 6 M (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]) \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6).
+definition Lam ≝ λx:\ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.λM:\ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6.\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"\ 6Abs\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/vclose.fix(0,0,4)"\ 6vclose\ 5/a\ 6 M \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6x\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6).
definition Judg ≝ λG,M.\ 5a href="cic:/matita/cr/lambda/vclose.fix(0,0,4)"\ 6vclose\ 5/a\ 6 M G \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.
definition body ≝ λx,M.match M with
- [ Abs M0 ⇒ \ 5a href="cic:/matita/cr/lambda/vopen.fix(0,0,2)"\ 6vopen\ 5/a\ 6 M (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]) \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6
+ [ Abs M0 ⇒ \ 5a href="cic:/matita/cr/lambda/vopen.fix(0,0,2)"\ 6vopen\ 5/a\ 6 M0 \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6x\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6
| _ ⇒ M ].
-inductive L (F:X → S_exp → Y) : S_exp → Prop \def
-| LPar : ∀x:X.L F (Par x)
-| LApp : ∀M,N:S_exp. (L F M) → (L F N) → L F (App M N)
-| LAbs : ∀M:S_exp. ∀x:X. (L F M) →
- L F (Abs (F x M) (subst_X M x (Var (F x M)))).
-
-definition apartb : X → S_exp → bool ≝
- λx,M.notb (mem X (N_eqb X) x (GV M)).
-
-let rec E (x:X) (M:S_exp) on M : list Y ≝
- match M with
- [ Par x ⇒ []
- | Var _ ⇒ []
- | App u v ⇒ E x u @ E x v
- | Abs y u ⇒ match apartb x u with
- [ true ⇒ []
- | false ⇒ y :: E x u ]].
-
-definition apart : X → S_exp → Prop ≝
- λx,M.¬ x ∈ GV M.
-
-interpretation "name apartness wrt GV" 'apart x s = (apart x s).
+inductive dupfree (A:Type[0]) : \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A → Prop ≝
+| df_nil : dupfree A [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6
+| df_cons : ∀x,xl.x \ 5a title="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 xl → dupfree A xl → dupfree A (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6xl).
-lemma apartb_true_to_apart : ∀x,s.apartb x s = true → x # s.
-intros;intro;
-lapply (in_list_to_mem_true ? (N_eqb X) ??? H1)
-[simplify;intro;generalize in match (p_eqb2 ? x1 x1);
- cases (x1 ≟ x1);intro;try autobatch;
- elim H2;reflexivity;
-|unfold apartb in H;rewrite > Hletin in H;simplify in H;destruct]
-qed.
-
-lemma apart_to_apartb_true : ∀x,s.x # s → apartb x s = true.
-intros;cut (¬ (mem X (N_eqb X) x (GV s)) = true)
-[unfold apartb;generalize in match Hcut;
- cases (mem X (N_eqb X) x (GV s));intro;
- [elim H1;reflexivity
- |reflexivity]
-|intro;apply H;autobatch]
-qed.
-
-lemma E_fresh : ∀x,M.x # M → E x M = [].
-intros 2;elim M;simplify
-[1,2:reflexivity
-|rewrite > H
- [rewrite > H1
- [reflexivity
- |elim s1 in H2;simplify;
- [simplify in H2;intro;apply H2;autobatch
- |autobatch
- |simplify in H4;intro;apply H4;autobatch
- |simplify in H3;intro;apply H3;autobatch]]
- |elim s in H2;simplify;
- [simplify in H2;intro;apply H2;lapply (in_list_singleton_to_eq ??? H3);
- autobatch
- |autobatch
- |simplify in H4;intro;apply H4;autobatch
- |simplify in H3;intro;apply H3;autobatch]]
-|rewrite > H
- [rewrite > (apart_to_apartb_true ?? H1);simplify;reflexivity
- |apply H1]]
-qed.
-
-lemma mem_false_to_not_in_list :
- ∀A,equ.(∀x,y.x = y → equ x y = true) →
- ∀x,l.mem A equ x l = false → x ∉ l.
-intros 5;elim l
-[autobatch
-|intro;apply (bool_elim ? (equ x a));intros
- [simplify in H2;rewrite > H4 in H2;simplify in H2;destruct
- |cases (in_list_cons_case ???? H3)
- [rewrite > H in H4
- [destruct
- |assumption]
- |apply H1;
- [generalize in match H2;simplify;rewrite > H4;simplify;
- intro;assumption
- |assumption]]]]
-qed.
+record df_list (A:Type[0]) : Type[0] ≝ {
+ list_of_dfl :> \ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A;
+ dfl_dupfree : \ 5a href="cic:/matita/cr/lambda/dupfree.ind(1,0,1)"\ 6dupfree\ 5/a\ 6 A list_of_dfl
+}.
-lemma mem_append : ∀A,equ.
- (∀x,y. x = y → equ x y = true) →
- (∀x,y. equ x y = true → x = y) →
- ∀x,l1,l2.mem A equ x (l1@l2) = orb (mem A equ x l1) (mem A equ x l2).
-intros;apply (bool_elim ? (mem A equ x (l1@l2)));intro
-[cut (x ∈ l1@l2)
- [cases (in_list_append_to_or_in_list ???? Hcut)
- [rewrite > in_list_to_mem_true
- [reflexivity
- |intro;apply H;reflexivity
- |assumption]
- |cases (mem A equ x l1);simplify;try reflexivity;
- rewrite > in_list_to_mem_true
- [reflexivity
- |intro;apply H;reflexivity
- |assumption]]
- |autobatch]
-|lapply (mem_false_to_not_in_list ????? H2)
- [assumption
- |apply orb_elim;apply (bool_elim ? (mem A equ x l1));intro;simplify
- [lapply (mem_true_to_in_list ????? H3);try assumption;
- elim Hletin;autobatch
- |apply (bool_elim ? (mem A equ x l2));intro;simplify
- [lapply (mem_true_to_in_list ????? H4);try assumption;
- elim Hletin;autobatch
- |reflexivity]]]]
-qed.
+(* ciascuno dei pre_tm utilizzati nella costruzione deve essere un ext_tm 0 *)
+inductive tm : \ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6 → Prop ≝
+| tm_Par : ∀xl:\ 5a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"\ 6df_list\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.∀x.x \ 5a title="list member" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 xl → tm (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"\ 6Par\ 5/a\ 6 x))
+| tm_App : ∀xl:\ 5a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"\ 6df_list\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.∀M1,M2:\ 5a href="cic:/matita/cr/lambda/ext_tm.ind(1,0,1)"\ 6ext_tm\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.tm (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl M1) → tm (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl M2) → tm (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"\ 6App\ 5/a\ 6 M1 M2))
+| tm_Lam : ∀xl:\ 5a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"\ 6df_list\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.∀x.∀M:\ 5a href="cic:/matita/cr/lambda/ext_tm.ind(1,0,1)"\ 6ext_tm\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.x \ 5a title="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 xl → tm (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 (x\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6xl) M) → tm (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl (\ 5a href="cic:/matita/cr/lambda/Lam.def(5)"\ 6Lam\ 5/a\ 6 x M)).
+
+(* I see no point in using cofinite quantification here *)
+inductive tm2 : \ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6 → Prop ≝
+| tm2_Par : ∀xl:\ 5a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"\ 6df_list\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.∀x.x \ 5a title="list member" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 xl → tm2 (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"\ 6Par\ 5/a\ 6 x))
+| tm2_App : ∀xl:\ 5a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"\ 6df_list\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.∀M1,M2.tm2 (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl M1) → tm2 (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl M2) → tm2 (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"\ 6App\ 5/a\ 6 M1 M2))
+| tm2_Lam : ∀xl:\ 5a href="cic:/matita/cr/lambda/df_list.ind(1,0,1)"\ 6df_list\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.∀M.(∀x.x \ 5a title="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 xl → tm2 (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 (x:\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6xl) (\ 5a href="cic:/matita/cr/lambda/body.def(3)"\ 6body\ 5/a\ 6 x (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"\ 6Abs\ 5/a\ 6 M)))) → tm2 (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"\ 6Abs\ 5/a\ 6 M)).
-(* lemma apartb_App_apart1 : ∀x,M,N.apartb x (App M N) = true → apartb x M = true.
-simplify;intros;unfold apartb;
-apply (bool_elim ? (mem X (N_eqb X) x (GV M)));
-simplify;intro
-[
-
-cut (x ∉ GV M @ GV N)
-[cut (apartb x M = false → False)
- [generalize in match Hcut1;cases (apartb x M);simplify;intro;
- [reflexivity|elim H1;reflexivity]
- |intro;apply Hcut;
-
-
-lemma apartb_App_apart1 : ∀x,M,N.apartb x (App M N) = true → apartb x M = true.
-
-lemma apartb_App_apart1 : ∀x,M,N.apartb x (App M N) = true → apartb x M = true.*)
-
-axiom daemon : False.
-
-lemma Ep : ∀x1,x2,M,Q.x1 ≠ x2 → x1 # Q → E x1 M = E x1 (subst_X M x2 Q).
-intros;elim M
-[simplify;cases (x2 ≟ c);simplify;autobatch
-|reflexivity
-|simplify;autobatch
-|whd in ⊢ (??%?);rewrite > H2;
- simplify in ⊢ (???%);
- rewrite > (? : apartb x1 s = apartb x1 (subst_X s x2 Q))
- [reflexivity
- |elim s
- [simplify;simplify in H2;apply (bool_elim ? (x1 ≟ c1));simplify;intro
- [apply (bool_elim ? (x2 ≟ c1));simplify;intro
- [lapply (p_eqb1 ??? H3);elim H;autobatch;
- |rewrite > H3;reflexivity]
- |apply (bool_elim ? (x2 ≟ c1));simplify;intro
- [autobatch
- |rewrite > H3;reflexivity]]
- |reflexivity
- |simplify;rewrite > mem_append
- [rewrite > mem_append
- [unfold apartb in H3;unfold apartb in H4;autobatch paramodulation
- |*:autobatch]
- |*:autobatch]
- |apply H3]]]
-qed.
+definition apartb : \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6 → \ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6 → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 ≝
+ λx,M.\ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/mem.fix(0,3,1)"\ 6mem\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/N_eqb.fix(0,0,2)"\ 6N_eqb\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6) x (\ 5a href="cic:/matita/cr/lambda/GV.fix(0,0,2)"\ 6GV\ 5/a\ 6 M)).
-lemma pi_Abs : ∀pi,x,M.pi · Abs x M = Abs x (pi · M).
-intros;reflexivity;
-qed.
+definition apart : \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6 → \ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"\ 6pre_tm\ 5/a\ 6 → Prop ≝
+ λx,M.x \ 5a title="list not member" href="cic:/fakeuri.def(1)"\ 6∉\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/GV.fix(0,0,2)"\ 6GV\ 5/a\ 6 M.
-lemma E_Abs : ∀x,y,v,M.y ∈ E x (Abs v M) → y ∈ v::E x M.
-intros 4;simplify;cases (apartb x M);simplify;intro
-[elim (not_in_list_nil ?? H)
-|assumption]
-qed.
+interpretation "name apartness wrt GV" 'apart x s = (apart x s).
-lemma E_all_fresh : ∀x1,x2,x3,M.
- x3 ≠ x1 → x3 ≠ x2 → E x3 M = E x3 (subst_X M x1 (Par x2)).
-intros;elim M;simplify
-[cases (x1 ≟ c);reflexivity
-|reflexivity
-|autobatch paramodulation
-|rewrite > (? : apartb x3 s = apartb x3 (subst_X s x1 (Par x2)))
- [rewrite > H2;reflexivity
- |elim s
- [simplify;simplify in H2;apply (bool_elim ? (x1 ≟ c1));simplify;intro
- [lapply (p_eqb1 ??? H3);rewrite < Hletin;
- rewrite > p_eqb4 [|assumption]
- rewrite > p_eqb4 [|assumption]
- reflexivity
- |reflexivity]
- |reflexivity
- |simplify;rewrite > mem_append
- [rewrite > mem_append
- [unfold apartb in H3;unfold apartb in H4;
- autobatch paramodulation
- |*:autobatch]
- |*:autobatch]
- |apply H3]]]
+lemma apartb_true_to_apart : ∀x,s.\ 5a href="cic:/matita/cr/lambda/apartb.def(3)"\ 6apartb\ 5/a\ 6 x s \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → x \ 5a title="name apartness wrt GV" href="cic:/fakeuri.def(1)"\ 6#\ 5/a\ 6 s.
+#x #s #H1 % #H2
+lapply (\ 5a href="cic:/matita/cr/lambda/in_list_to_mem_true.dec"\ 6in_list_to_mem_true\ 5/a\ 6 ? (\ 5a href="cic:/matita/cr/lambda/N_eqb.fix(0,0,2)"\ 6N_eqb\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6) … H2) //
+#Hletin normalize in H1; >Hletin in H1;
+normalize #Hfalse destruct (Hfalse)
qed.
-lemma E_fresh_subst_Y :
- ∀x1,x2,y,S.x1 ≠ x2 → E x1 S = E x1 (subst_Y S y (Par x2)).
-intros;elim S
-[reflexivity
-|simplify;cases (y ≟ c);simplify;reflexivity
-|simplify;autobatch paramodulation
-|simplify;apply (bool_elim ? (y ≟ c));intro;simplify
- [reflexivity
- |rewrite < H1;rewrite < (? : apartb x1 s = apartb x1 (subst_Y s y (Par x2)))
- [reflexivity
- |elim s;simplify
- [reflexivity
- |cases (y ≟ c1);simplify
- [rewrite > p_eqb4;autobatch
- |reflexivity]
- |rewrite > mem_append [|*:autobatch]
- rewrite > mem_append [|*:autobatch]
- unfold apartb in H3;unfold apartb in H4;
- autobatch paramodulation
- |cases (y ≟ c1); simplify
- [reflexivity
- |apply H3]]]]]
+lemma apart_to_apartb_true : ∀x,s.x \ 5a title="name apartness wrt GV" href="cic:/fakeuri.def(1)"\ 6#\ 5/a\ 6 s → \ 5a href="cic:/matita/cr/lambda/apartb.def(3)"\ 6apartb\ 5/a\ 6 x s \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
+#x #s #H1 normalize
+>(\ 5a href="cic:/matita/cr/lambda/not_in_list_to_mem_false.def(4)"\ 6not_in_list_to_mem_false\ 5/a\ 6 ????? H1) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"\ 6p_eqb1\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
qed.
-lemma subst_X_apart : ∀x,M,N. x # M → subst_X M x N = M.
-intros 2;
-elim M
-[simplify;simplify in H;
- rewrite > p_eqb4
- [reflexivity
- |intro;apply H;autobatch]
-|reflexivity
-|simplify;rewrite > H
- [rewrite > H1
- [reflexivity
- |intro;apply H2;simplify;autobatch]
- |intro;apply H2;simplify;autobatch]
-|simplify;rewrite >H
- [reflexivity
- |apply H1]]
+lemma pi_Abs : ∀pi,M.pi \ 5a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"\ 6Abs\ 5/a\ 6 M \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"\ 6Abs\ 5/a\ 6 (pi \ 5a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 M).
+#pi #M %
qed.
-lemma subst_Y_not_dangling : ∀y,M,N. y ∉ LV M → subst_Y M y N = M.
-intros 2;
-elim M
-[reflexivity
-|simplify;simplify in H;
- rewrite > p_eqb4
- [reflexivity
- |intro;apply H;autobatch]
-|simplify;rewrite > H
- [rewrite > H1
- [reflexivity
- |intro;apply H2;simplify;autobatch]
- |intro;apply H2;simplify;autobatch]
-|simplify;simplify in H1;apply (bool_elim ? (y ≟ c));simplify;intro
- [reflexivity
- |rewrite > H
- [reflexivity
- |intro;apply H1;apply in_list_filter_r;autobatch]]]
+lemma subst_apart : ∀x,M,N. x \ 5a title="name apartness wrt GV" href="cic:/fakeuri.def(1)"\ 6#\ 5/a\ 6 M → \ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 M x N \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 M.
+#x #M elim M
+[ normalize #x0 #N #H1 >\ 5a href="cic:/matita/cr/lambda/p_eqb4.def(4)"\ 6p_eqb4\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6, \ 5a href="cic:/matita/cr/lambda/in_list.con(0,1,1)"\ 6in_list_head\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+| #n #N #H1 %
+| normalize #M1 #M2 #IH1 #IH2 #N #H1 >IH1 /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6, \ 5a href="cic:/matita/cr/lambda/incl_append_l.dec"\ 6incl_append_l\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ >IH2 /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6, \ 5a href="cic:/matita/cr/lambda/incl_append_r.dec"\ 6incl_append_r\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+| normalize #M0 #IH #N #H1 >IH /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
+]
qed.
-lemma subst_X_lemma :
- ∀x1,x2,M,P,Q.x1 ≠ x2 → x1 # Q →
- subst_X (subst_X M x1 P) x2 Q = subst_X (subst_X M x2 Q) x1 (subst_X P x2 Q).
-intros;elim M
-[simplify;apply (bool_elim ? (x1 ≟ c));simplify;intro
- [rewrite > p_eqb4
- [simplify;rewrite > H2;reflexivity
- |intro;autobatch]
- |apply (bool_elim ? (x2 ≟ c));simplify;intro
- [rewrite > subst_X_apart;autobatch
- |rewrite > H2;reflexivity]]
-|reflexivity
-|*:simplify;autobatch paramodulation]
+lemma subst_lemma :
+ ∀x1,x2,M,P,Q.x1 \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 x2 → x1 \ 5a title="name apartness wrt GV" href="cic:/fakeuri.def(1)"\ 6#\ 5/a\ 6 Q →
+ \ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 M x1 P) x2 Q \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 M x2 Q) x1 (\ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 P x2 Q).
+#x1 #x2 #M #P #Q #H1 #H2 elim M
+[ #x0 normalize @(\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"\ 6bool_elim\ 5/a\ 6 ? (x1 \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 x0)) normalize #H3
+ [ >\ 5a href="cic:/matita/cr/lambda/p_eqb4.def(4)"\ 6p_eqb4\ 5/a\ 6
+ [ normalize >H3 normalize %
+ | @(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … H1) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"\ 6p_eqb1\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ ]
+ | @(\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"\ 6bool_elim\ 5/a\ 6 ? (x2 \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 x0)) normalize #H4 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/cr/lambda/subst_apart.def(5)"\ 6subst_apart\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ >H3 normalize %
+ ]
+| *: // normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
+]
qed.
-lemma subst_cancel : ∀x,y,M.x # M → M = subst_X (subst_Y M y (Par x)) x (Var y).
+(* was: subst_cancel *)
+(* won't prove it now because it's unsure if we need a more general version,
+ with a list xl instead of [x], and/or with a generic n instead of O *)
+axiom vopen_vclose_cancel : ∀x,M.x \ 5a title="name apartness wrt GV" href="cic:/fakeuri.def(1)"\ 6#\ 5/a\ 6 M → M \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/vclose.fix(0,0,4)"\ 6vclose\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/vopen.fix(0,0,2)"\ 6vopen\ 5/a\ 6 M \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6x\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6) \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6x\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6.
+(*
intros 3;elim M
[simplify;simplify in H;rewrite > p_eqb4
[reflexivity
|rewrite < H
[reflexivity
|apply H1]]]
-qed.
-
-lemma subst_X_merge : ∀M,N,x1,x2.x2 # M →
- subst_X (subst_X M x1 (Par x2)) x2 N = subst_X M x1 N.
-intros 4;elim M
-[simplify;apply (bool_elim ? (x1 ≟ c));simplify;intro
- [rewrite > Neqb_n_n;reflexivity
- |rewrite > p_eqb4
- [reflexivity
- |intro;elim H;simplify;autobatch]]
-|reflexivity
-|simplify;simplify in H2;rewrite > H
- [rewrite > H1
- [reflexivity
- |intro;autobatch]
- |intro;autobatch]
-|simplify;rewrite > H
- [reflexivity
- |apply H1]]
-qed.
-
-lemma subst_X_Y_commute : ∀x1,x2,y,M,N. x1 ≠ x2 → y ∉ LV N →
- subst_Y (subst_X M x1 N) y (Par x2) = subst_X (subst_Y M y (Par x2)) x1 N.
-intros;elim M
-[simplify;apply (bool_elim ? (x1 ≟ c));simplify;intro
- [rewrite > subst_Y_not_dangling;autobatch
- |reflexivity]
-|simplify;apply (bool_elim ? (y ≟ c));simplify;intro
- [rewrite > p_eqb4
- [reflexivity
- |assumption]
- |reflexivity]
-|simplify;autobatch paramodulation
-|simplify;apply (bool_elim ? (y ≟ c));simplify;intro
- [reflexivity
- |rewrite < H2;reflexivity]]
-qed.
-
-inductive LL (F : X → S_exp → Y) : S_exp → Prop ≝
-| LLPar : ∀x.LL F (Par x)
-| LLApp : ∀M,N.LL F M → LL F N → LL F (App M N)
-| LLAbs : ∀x1,M.(∀x2.(x2 ∈ GV M → x2 = x1) → LL F (subst_X M x1 (Par x2))) →
- LL F (Abs (F x1 M) (subst_X M x1 (Var (F x1 M)))).
-
-include "nat/compare.ma".
-
-definition max : nat → nat → nat ≝
- λx,y.match leb x y with
- [ true ⇒ y
- | false ⇒ x ].
-
-let rec S_len M ≝ match M with
-[ Par _ ⇒ O
-| Var _ ⇒ O
-| App N P ⇒ S (max (S_len N) (S_len P))
-| Abs x N ⇒ S (S_len N) ].
-
-lemma S_len_ind :
- ∀P:S_exp → Prop.
- (∀M.(∀N.S_len N < S_len M → P N) → P M)
- → ∀M.P M.
-intros;
-cut (∀N.S_len N ≤ S_len M → P N)
-[|elim M 0;simplify;intros
- [1,2:apply H;intros;elim (not_le_Sn_O (S_len N1));autobatch
- |apply H;intros;generalize in match (trans_le ??? H4 H3);unfold max;
- apply (bool_elim ? (leb (S_len s) (S_len s1)));simplify;intros;autobatch
- |apply H;intros;apply H1;apply le_S_S_to_le;autobatch]]
-apply H;intros;autobatch;
-qed.
-
-record height : Type ≝
-{
- H : X → S_exp → Y;
- HE : ∀M:S_exp. ∀x:X. ∀pi:Pi. (L H M) → H x M = H (pi x) (pi · M);
- HF : ∀M:S_exp. ∀x:X. (L H M) → H x M ∉ E x M;
- HP : ∀M,Q:S_exp. ∀x1,x2:X. (L H M) → (L H Q) → (x1 ≟ x2) = false →
- apartb x1 Q = true → (H x1 M ≟ H x1 (subst_X M x2 Q)) = true
-}.
-coercion H 2.
-
-record xheight : Type ≝
-{
- XH : X → S_exp → Y;
- XHE : ∀M:S_exp. ∀x:X. ∀pi:Pi. XH x M = XH (pi x) (pi · M);
- XHF : ∀M:S_exp. ∀x:X. XH x M ∉ E x M;
- XHP : ∀M,Q:S_exp. ∀x1,x2:X.(x1 ≟ x2) = false →
- apartb x1 Q = true → (XH x1 M ≟ XH x1 (subst_X M x2 Q)) = true
-}.
-coercion XH 2.
-
-include "logic/coimplication.ma".
-
-definition coincl : ∀A.list A → list A → Prop ≝ λA,l1,l2.∀x.x ∈ l1 ↔ x ∈ l2.
-
-notation > "hvbox(a break ≡ b)"
- non associative with precedence 45
-for @{'equiv $a $b}.
-
-notation < "hvbox(term 46 a break ≡ term 46 b)"
- non associative with precedence 45
-for @{'equiv $a $b}.
-
-interpretation "list coinclusion" 'equiv x y = (coincl ? x y).
-
-lemma refl_coincl : ∀A.∀l:list A.l ≡ l.
-intros;intro;split;intro;assumption;
-qed.
-
-lemma filter_append : ∀A,l1,l2,p.filter A (l1@l2) p = filter A l1 p @ filter A l2 p.
-intros;elim l1
-[reflexivity
-|simplify;cases (p a);simplify;rewrite < H;reflexivity]
-qed.
-
-lemma GV_subst_X_Var :
- ∀M,x,y. GV (subst_X M x (Var y)) ≡ filter ? (GV M) (λz.¬(x ≟ z)).
-intros;elim M;simplify
-[cases (x ≟ c);simplify;autobatch
-|autobatch
-|intro;split;intro
- [rewrite > filter_append;cases (in_list_append_to_or_in_list ???? H2)
- [cases (H x1);autobatch
- |cases (H1 x1);autobatch]
- |rewrite > filter_append in H2;cases (in_list_append_to_or_in_list ???? H2)
- [cases (H x1);autobatch
- |cases (H1 x1);autobatch]]
-|intro;split;intro;cases (H x1);autobatch]
-qed.
-
-lemma swap_GV : ∀x,M. x ∈ GV M → ∀x1,x2.swap X x1 x2 x ∈ GV (pi_swap X x1 x2 · M).
-intros;elim M in H
-[simplify;simplify in H;rewrite > (in_list_singleton_to_eq ??? H);autobatch
-|simplify in H;elim (not_in_list_nil ?? H)
-|simplify in H2;simplify;cases (in_list_append_to_or_in_list ???? H2);autobatch
-|simplify in H1;simplify;autobatch]
-qed.
+qed. *)
-(* easy to prove, but not needed *)
-lemma L_swap : ∀F:xheight.∀M.L F M →
- ∀x1,x2.L F (pi_swap ? x1 x2 · M).
-intros;elim H
-[simplify;autobatch
-|simplify;autobatch
-|simplify;rewrite > pi_lemma1;simplify;
- rewrite > (?: F c s = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s))
- [apply LAbs;assumption
- |autobatch;]]
+lemma subst_merge : ∀M,N,x1,x2.x2 \ 5a title="name apartness wrt GV" href="cic:/fakeuri.def(1)"\ 6#\ 5/a\ 6 M →
+ \ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 M x1 (\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"\ 6Par\ 5/a\ 6 x2)) x2 N \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 M x1 N.
+#M #N #x1 #x2 elim M
+[normalize #x0 @(\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"\ 6bool_elim\ 5/a\ 6 ? (x1 \ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"\ 6≟\ 5/a\ 6 x0)) normalize #H1
+ [ >\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"\ 6Neqb_n_n\ 5/a\ 6 normalize //
+ | #H2 >\ 5a href="cic:/matita/cr/lambda/p_eqb4.def(4)"\ 6p_eqb4\ 5/a\ 6 normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6, \ 5a href="cic:/matita/cr/lambda/in_list.con(0,1,1)"\ 6in_list_head\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ ]
+|#n #H1 %
+|#M1 #M2 #IH1 #IH2 normalize #H1 >IH1 /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6, \ 5a href="cic:/matita/cr/lambda/incl_append_l.dec"\ 6incl_append_l\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ >IH2 /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6, \ 5a href="cic:/matita/cr/lambda/incl_append_r.dec"\ 6incl_append_r\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+|#M0 #IH normalize #H1 >IH /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/
+]
qed.
-lemma LL_swap : ∀F:xheight.∀M.LL F M →
- ∀x1,x2.LL F (pi_swap ? x1 x2 · M).
-intros;elim H
-[simplify;autobatch
-|simplify;autobatch
-|simplify;rewrite > pi_lemma1;simplify;
- rewrite > (?: F c s = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s))
- [apply LLAbs;intros;lapply (H2 (pi_swap ? x1 x2 x))
- [rewrite > (?: Par x = pi_swap ? x1 x2 · (Par (pi_swap ? x1 x2 x)))
- [autobatch
- |elim daemon (*involution*)]
- |intro;rewrite < (swap_inv ? x1 x2 c);
- rewrite < eq_swap_pi;apply eq_f;rewrite > eq_swap_pi;apply H3;
- rewrite < (swap_inv ? x1 x2 x);autobatch]
- |autobatch]]
-qed.
+(* was: subst_X_Y_commute
+ won't prove it now, it's not easy to understand if it's needed and in which form *)
+axiom subst_vopen_commute : ∀x1,x2,M,N. x1 \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 x2 →
+ \ 5a href="cic:/matita/cr/lambda/vopen.fix(0,0,2)"\ 6vopen\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 M x1 N) \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6x2\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"\ 6subst\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/vopen.fix(0,0,2)"\ 6vopen\ 5/a\ 6 M \ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6x2\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6) x1 N.
-(*lemma LL_subst_X : ∀F:xheight.∀M.LL F M →
- ∀x1,x2.LL F (subst_X M x1 (Par x2)).
-intros 2;apply (S_len_ind ?? M);intro;cases M1;simplify;intros
-[cases (x1 ≟ c);simplify;autobatch
-|inversion H1;simplify;intros;destruct
-|inversion H1;simplify;intros;destruct;
- clear H3 H5;apply LLApp;apply H;try assumption
- [(* len *)elim daemon
- |(* len *)elim daemon]
-|inversion H1;simplify;intros;destruct;
- unfold lam in H4;clear H3;destruct;
- apply (bool_elim ? (x1 ≟ c1));intro
- [rewrite > subst_X_apart
- [assumption
- |intro;rewrite > (?: (x1 ≟ c1) = false) in H3
- [destruct
- |elim (GV_subst_X_Var s1 c1 (F c1 s1) x1);
- lapply (H5 H4);lapply (in_list_filter_to_p_true ???? Hletin);
- apply p_eqb4;intro;rewrite > H7 in Hletin1;
- rewrite > Neqb_n_n in Hletin1;simplify in Hletin1;destruct]]
- |letin c2 ≝ (N_fresh ? (x1::x2::c1::GV s1));
- cut (c2 ∉ (x1::x2::c1::GV s1)) as Hc2 [|apply p_fresh]
- clearbody c2;
- rewrite > (? : s1 = subst_X (subst_X s1 c1 (Par c2)) c2 (Par c1)) in ⊢ (? ? (? ? (? (? % ? ?) ? ?)))
- [|rewrite > subst_X_merge
- [autobatch
- |intro;apply Hc2;autobatch depth=4]]
- rewrite > (? : F c1 s1 = F c2 (subst_X s1 c1 (Par c2)))
- [|rewrite > subst_X_fp
- [rewrite < (swap_left ? c1 c2) in ⊢ (? ? ? (? ? % ?));
- rewrite > eq_swap_pi;autobatch
- |intro;elim Hc2;autobatch depth=4]]
- rewrite > subst_X_merge
- [|intro;apply Hc2;do 2 apply in_list_cons;generalize in match H4;
- elim s1 0;simplify;intros
- [apply (bool_elim ? (c1 ≟ c));intro;
- rewrite > H6 in H5;simplify in H5;
- lapply (in_list_singleton_to_eq ??? H5)
- [rewrite > Hletin;autobatch
- |rewrite > Hletin in H6;rewrite > Neqb_n_n in H6;destruct]
- |elim (not_in_list_nil ?? H5)
- |cases (in_list_append_to_or_in_list ???? H7)
- [cases (in_list_cons_case ???? (H5 H8));autobatch
- |cases (in_list_cons_case ???? (H6 H8));autobatch]
- |autobatch]]
- rewrite > (subst_X_lemma c2 x1 ? ??)
- [simplify;rewrite > (? : F c2 (subst_X s1 c1 (Par c2)) = F c2 (subst_X (subst_X s1 c1 (Par c2)) x1 (Par x2)))
- [|apply p_eqb1;apply XHP;
- [apply p_eqb4;intro;apply Hc2;autobatch
- |simplify;rewrite > (? : (c2 ≟ x2) = false)
- [reflexivity
- |apply p_eqb4;intro;apply Hc2;autobatch]]]
- apply LLAbs;
- intros (x3);
- apply H
- [(*len*)elim daemon
- |3:assumption
- |apply H
- [(*len*)elim daemon
- |apply H2;intro;elim Hc2;autobatch depth=4]]
- |intro;apply Hc2;autobatch
- |simplify;intro;elim Hc2;rewrite > (? : c2 = x2);autobatch]]]
-qed.*)
+axiom daemon : ∀P:Prop.P.
-lemma L_to_LL : ∀M.∀F:xheight.L F M → LL F M.
-intros;elim H
-[autobatch
-|autobatch
-|apply LLAbs;intros;rewrite > subst_X_fp;autobatch]
+lemma GV_tm_nil : ∀I.\ 5a href="cic:/matita/cr/lambda/tm.ind(1,0,0)"\ 6tm\ 5/a\ 6 I → \ 5a href="cic:/matita/cr/lambda/GV.fix(0,0,2)"\ 6GV\ 5/a\ 6 I \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6.
+#I #H1 elim H1 normalize
+[ #xl #x #Hx (* posn_in_elim *) @\ 5a href="cic:/matita/cr/lambda/daemon.dec"\ 6daemon\ 5/a\ 6
+| #xl #M1 #M2 #H1 #H2 #IH1 #IH2 >IH1 >IH2 %
+| #xl #x #M #H1 #H2 #IH1
+ (* prove vclose (vclose M xl n) yl |xl| = vclose M (xl@yl) n *)
+ @\ 5a href="cic:/matita/cr/lambda/daemon.dec"\ 6daemon\ 5/a\ 6
+]
qed.
-lemma LL_to_L : ∀M.∀F:xheight.LL F M → L F M.
-intros;elim H
-[1,2:autobatch
-|apply LAbs;lapply (H2 c)
- [rewrite > subst_X_x_x in Hletin;assumption
- |intro;reflexivity]]
+definition fp_list ≝ λpi:\ 5a href="cic:/matita/cr/lambda/fp.ind(1,0,1)"\ 6fp\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.λxl:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6.\ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"\ 6map\ 5/a\ 6 ?? pi xl.
+interpretation "apply fp list" 'middot pi xl = (fp_list pi xl).
+
+(* is it really necessary? *)
+lemma pi_no_support : ∀pi,M.\ 5a href="cic:/matita/cr/lambda/GV.fix(0,0,2)"\ 6GV\ 5/a\ 6 M \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 [\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6]\ 5/a\ 6 → pi\ 5a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6M \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 M.
+#pi #M elim M
+[ normalize #x0 #H1 destruct (H1)
+| normalize //
+| #M1 #M2 #IH1 #IH2 normalize #H1 >IH1
+ [ >IH2 //
+ cases (\ 5a href="cic:/matita/cr/lambda/GV.fix(0,0,2)"\ 6GV\ 5/a\ 6 M1) in H1; normalize //
+ #x0 #xl0 #H1 destruct (H1)
+ | cases (\ 5a href="cic:/matita/cr/lambda/GV.fix(0,0,2)"\ 6GV\ 5/a\ 6 M1) in H1; //
+ #x0 #xl0 normalize #H1 destruct (H1)
+ ]
+| normalize #M0 #IH0 #H1 >IH0 //
+]
qed.
-lemma subst_X_decompose :
- ∀x,y,M,N.y ∉ LV M → y ∉ E x M →
- subst_X M x N = subst_Y (subst_X M x (Var y)) y N.
-intros 3;elim M
-[simplify;cases (x ≟ c);simplify;
- [rewrite > p_eqb3;autobatch
- |reflexivity]
-|simplify;simplify in H;
- rewrite > p_eqb4;
- [reflexivity
- |intro;apply H;autobatch]
-|simplify;rewrite < H
- [rewrite < H1
- [reflexivity
- |intro;apply H2;simplify;autobatch
- |intro;apply H3;simplify;autobatch]
- |intro;apply H2;simplify;autobatch
- |intro;apply H3;simplify;autobatch]
-|simplify;apply (bool_elim ? (y ≟ c));intros;
- [simplify;apply (bool_elim ? (apartb x s))
- [intro;simplify;
- lapply (apartb_true_to_apart ?? H4);
- rewrite > subst_X_apart
- [rewrite > subst_X_apart
- [reflexivity
- |assumption]
- |assumption]
- |intro;simplify in H2;rewrite > H4 in H2;
- simplify in H2;elim H2;
- rewrite > (p_eqb1 ??? H3);autobatch]
- |simplify;rewrite < H;
- [reflexivity
- |generalize in match H1;simplify;elim (LV s)
- [autobatch
- |intro;cases (in_list_cons_case ???? H6)
- [elim H5;simplify;rewrite < H7;rewrite > H3;simplify;autobatch
- |elim (H4 ? H7);intro;apply H5;simplify;cases (¬ (a ≟ c));simplify;autobatch]]
- |intro;apply H2;simplify;apply (bool_elim ? (apartb x s));intro
- [simplify;rewrite > E_fresh in H4
- [assumption
- |autobatch]
- |simplify;autobatch]]]]
+lemma posn_eqv : ∀pi,xl,x.\ 5a href="cic:/matita/cr/lambda/posn.fix(0,1,3)"\ 6posn\ 5/a\ 6 ? (pi\ 5a title="apply fp list" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6xl) (pi x) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/posn.fix(0,1,3)"\ 6posn\ 5/a\ 6 ? xl x.
+#pi #xl #x @\ 5a href="cic:/matita/cr/lambda/daemon.dec"\ 6daemon\ 5/a\ 6
qed.
-lemma subst_Y_decompose :
- ∀x,y,M,N.x # M →
- subst_Y M y N = subst_X (subst_Y M y (Par x)) x N.
-intros 3;elim M
-[simplify;simplify in H;rewrite > p_eqb4
- [reflexivity
- |intro;apply H;autobatch]
-|simplify;apply (bool_elim ? (y ≟ c));simplify;intro
- [rewrite > Neqb_n_n;reflexivity
- |reflexivity]
-|simplify;rewrite < H
- [rewrite < H1
- [reflexivity
- |intro;apply H2;simplify;autobatch]
- |intro;apply H2;simplify;autobatch]
-|simplify;simplify in H1;apply (bool_elim ? (y ≟ c));simplify;intro
- [simplify;rewrite > subst_X_apart
- [reflexivity
- |assumption]
- |rewrite < H
- [reflexivity
- |apply H1]]]
+lemma vclose_eqv : ∀pi,M,xl,k.pi\ 5a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6\ 5a href="cic:/matita/cr/lambda/vclose.fix(0,0,4)"\ 6vclose\ 5/a\ 6 M xl k \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/vclose.fix(0,0,4)"\ 6vclose\ 5/a\ 6 (pi\ 5a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6M) (pi\ 5a title="apply fp list" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6xl) k.
+#pi #M #xl elim M
+[ #x0 #k normalize >\ 5a href="cic:/matita/cr/lambda/posn_eqv.def(4)"\ 6posn_eqv\ 5/a\ 6 cases (\ 5a href="cic:/matita/cr/lambda/posn.fix(0,1,3)"\ 6posn\ 5/a\ 6 \ 5a href="cic:/matita/cr/lambda/X.dec"\ 6X\ 5/a\ 6 xl x0) normalize //
+| #n0 #k %
+| #M1 #M2 #IH1 #IH2 #k whd in ⊢ (??%%); //
+| #M0 #IH0 #k whd in ⊢ (??%%); //
+]
qed.
-lemma pre_height : ∀x1,x2,y,M.y ∉ E x1 M → y ∉ LV M →
- subst_X M x1 (Par x2) = subst_Y (subst_X M x1 (Var y)) y (Par x2).
-intros;apply subst_X_decompose;assumption;
-qed.
+lemma tm_eqv : ∀pi,I.\ 5a href="cic:/matita/cr/lambda/tm.ind(1,0,0)"\ 6tm\ 5/a\ 6 I → pi\ 5a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6I \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 I.
+#pi #I #H1 elim H1
+[ #xl0 #x0 #Hx0
-lemma HL_conv : ∀x,y,M.y ∈ E x M → M ≠ subst_Y (subst_X M x (Var y)) y (Par x).
-intros 3;elim M
-[simplify in H;elim (not_in_list_nil ?? H);
-|simplify in H;elim (not_in_list_nil ?? H)
-|simplify;intro;simplify in H2;destruct;
- cases (in_list_append_to_or_in_list ???? H2);autobatch
-|simplify;simplify in H1;
- cut (apartb x s = false)
- [rewrite > Hcut in H1;simplify in H1;apply (bool_elim ? (y ≟ c));intro
- [simplify;intro;cut (¬ x # s)
- [apply Hcut1;generalize in match H3;elim s 0;simplify;
- [intro;apply (bool_elim ? (x ≟ c1));simplify;intros;
- [destruct
- |autobatch]
- |intros;autobatch
- |intros;destruct;intro;cases (in_list_append_to_or_in_list ???? H3)
- [apply H4
- [demodulate all
- |assumption]
- |apply H5
- [demodulate all
- |assumption]]
- |intros;destruct;apply H4;demodulate all]
- |intro;rewrite > (apart_to_apartb_true ?? H4) in Hcut;destruct]
- |simplify;intro;apply H
- [cases (in_list_cons_case ???? H1)
- [rewrite > p_eqb3 in H2
- [destruct
- |assumption]
- |assumption]
- |destruct;assumption]]
- |generalize in match H1;cases (apartb x s);simplify;intro
- [elim (not_in_list_nil ?? H2)
- |reflexivity]]]
-qed.
+theorem term_to_term2 : ∀xl,t.\ 5a href="cic:/matita/cr/lambda/tm.ind(1,0,0)"\ 6tm\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl t) → \ 5a href="cic:/matita/cr/lambda/tm2.ind(1,0,0)"\ 6tm2\ 5/a\ 6 (\ 5a href="cic:/matita/cr/lambda/Judg.def(5)"\ 6Judg\ 5/a\ 6 xl t).
+#xl #t #H elim H /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/cr/lambda/tm2.con(0,1,0)"\ 6tm2_Par\ 5/a\ 6, \ 5a href="cic:/matita/cr/lambda/tm2.con(0,2,0)"\ 6tm2_App\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+#xl0 #x0 #M #Hx #H1 #IH1 %3 #x1 #Hx1
+normalize in ⊢ (?(??%));
-let rec BV t ≝ match t with
- [ Par _ ⇒ []
- | Var _ ⇒ []
- | App t1 t2 ⇒ BV t1 @ BV t2
- | Abs y u ⇒ y::BV u ].
-
-lemma E_BV : ∀x,M.E x M ⊆ BV M.
-intros;elim M;simplify
-[1,2:unfold;intros;assumption
-|unfold;intros;cases (in_list_append_to_or_in_list ???? H2);autobatch
-|cases (apartb x s);simplify
- [unfold;intros;elim (not_in_list_nil ?? H1)
- |autobatch]]
-qed.
-
(*
-let rec L_check (F:xheight) M on M ≝ match M with
- [ Par _ ⇒ true
- | Var _ ⇒ false
- | App N P ⇒ andb (L_check F N) (L_check F P)
- | Abs y N ⇒ let X ≝ (N_fresh ? (GV M)) in
- andb (y ≟ F X (subst_Y N y (Par X)))
- (L_check F (subst_Y N y (Par X))) ].
-*)
-
-let rec L_check_aux (F:xheight) M n on n ≝ match n with
-[ O ⇒ false (* vacuous *)
-| S m ⇒ match M with
- [ Par _ ⇒ true
- | Var _ ⇒ false
- | App N P ⇒ andb (L_check_aux F N m) (L_check_aux F P m)
- | Abs y N ⇒ let X ≝ (N_fresh ? (GV M)) in
- andb (y ≟ F X (subst_Y N y (Par X)))
- (L_check_aux F (subst_Y N y (Par X)) m) ]].
-
-lemma L_check_aux_sound :
- ∀F,M,n.S_len M ≤ n → L_check_aux F M (S n) = true → L F M.
-intros 2;apply (S_len_ind ?? M);intro;cases M1;intros
-[autobatch
-|simplify in H2;destruct
-|simplify in H2;generalize in match H2;
- apply (andb_elim (L_check_aux F s n) (L_check_aux F s1 n));
- apply (bool_elim ? (L_check_aux F s n));simplify;intros
- [apply LApp
- [apply (H ?? (pred n))
- [simplify;(*len*)elim daemon
- |simplify in H1;generalize in match H1;cases n;intros
- [elim (not_le_Sn_O ? H5)
- |simplify;elim daemon (* H5 *)]
- |(* H3 *) elim daemon]
- |apply (H ?? (pred n))
- [simplify;(*len*) elim daemon
- |simplify in H1;generalize in match H1;cases n;intros
- [elim (not_le_Sn_O ? H5)
- |simplify;elim daemon (* H5 *)]
- |(* H4 *) elim daemon]]
- |destruct]
-|simplify in H2;generalize in match H2;clear H2;
- apply (andb_elim (c ≟ F (N_fresh X (GV s)) (subst_Y s c (Par (N_fresh X (GV s)))))
- (L_check_aux F (subst_Y s c (Par (N_fresh X (GV s)))) n));
- apply (bool_elim ? (c≟F (N_fresh X (GV s)) (subst_Y s c (Par (N_fresh X (GV s))))));
- simplify;intros
- [rewrite > (p_eqb1 ??? H2);
- rewrite > (? : s =
- subst_X
- (subst_Y s c
- (Par (N_fresh X (GV s))))
- (N_fresh X (GV s))
- (Var (F (N_fresh X (GV s)) (subst_Y s c (Par (N_fresh X (GV s)))))))
- in ⊢ (?? (?? %))
- [apply LAbs;apply (H ?? (pred n))
- [simplify;(*len*)elim daemon
- |simplify in H1;generalize in match H1;cases n;intros
- [elim (not_le_Sn_O ? H4)
- |simplify;elim daemon (* H4 *)]
- |rewrite > (? : S (pred n) = n)
- [assumption
- |(*arith*)elim daemon]]
- |rewrite < subst_Y_decompose
- [rewrite < (p_eqb1 ??? H2);autobatch
- |apply p_fresh]]
- |destruct]]
-qed.
-
-lemma LV_subst_X : ∀s,x,y. LV (subst_X s x (Var y)) ⊆ y::LV s.
-intros 3;elim s
-[simplify;cases (x ≟ c);simplify;
- [autobatch
- |unfold;intros;elim (not_in_list_nil ?? H)]
-|simplify;unfold;intros;autobatch
-|simplify;unfold;intros;
- cases (in_list_append_to_or_in_list ???? H2)
- [lapply (H ? H3);autobatch
- |lapply (H1 ? H3);cases (in_list_cons_case ???? Hletin)
- [applyS in_list_head
- |autobatch]]
-|simplify;unfold;intros;
- lapply (in_list_filter ???? H1);
- lapply (H ? Hletin);
- cases (in_list_cons_case ???? Hletin1)
- [rewrite > H2;autobatch
- |apply in_list_cons;apply in_list_filter_r
- [assumption
- |apply (in_list_filter_to_p_true ???? H1)]]]
-qed.
-
-lemma eq_list_nil : ∀A.∀l:list A.(∀x.x ∉ l) → l = [].
-intros 2;cases l;intro
-[reflexivity
-|elim (H a);autobatch]
-qed.
-
-(* to be revised *)
-lemma L_to_closed : ∀F:xheight.∀M.L F M → LV M = [].
-intros;elim H
-[reflexivity
-|simplify;autobatch paramodulation
-|simplify;generalize in match H2;generalize in match (F c s);elim s
- [simplify;apply (bool_elim ? (c ≟ c1));simplify;intro
- [rewrite > p_eqb3;reflexivity
- |reflexivity]
- |simplify in H3;destruct
- |simplify in H5;simplify;
- rewrite > (? :
- filter Y (LV (subst_X s1 c (Var c1))@LV (subst_X s2 c (Var c1))) (λz.¬(z≟c1)) =
- filter Y (LV (subst_X s1 c (Var c1))) (λz.¬(z≟c1))@ filter Y (LV (subst_X s2 c (Var c1))) (λz.¬(z≟c1)))
- [rewrite > H3
- [rewrite > H4
- [reflexivity
- |generalize in match H5;cases (LV s2);simplify;
- [intro;reflexivity
- |cases (LV s1);simplify;intro;destruct]]
- |generalize in match H5;cases (LV s1);simplify;intro
- [reflexivity
- |destruct]]
- |elim (LV (subst_X s1 c (Var c1)));simplify
- [reflexivity
- |cases (a ≟ c1);simplify;rewrite > H6;reflexivity]]
- |simplify;apply eq_list_nil;intro;intro;
- lapply (in_list_filter ???? H5) as H6;
- lapply (in_list_filter ???? H6) as H7;
- lapply (in_list_filter_to_p_true ???? H5) as H8;
- lapply (in_list_filter_to_p_true ???? H6) as H9;
- lapply (LV_subst_X ???? H7);
- cut (LV s1 ⊆ [c1])
- [cases (in_list_cons_case ???? Hletin)
- [rewrite > (p_eqb3 ??? H10) in H8;simplify in H8;destruct
- |lapply (Hcut ? H10);lapply (in_list_singleton_to_eq ??? Hletin1);
- rewrite > (p_eqb3 ??? Hletin2) in H9;simplify in H9;destruct]
- |simplify in H4;generalize in match H4;elim (LV s1) 0;simplify
- [intro;unfold;intros;elim (not_in_list_nil ?? H11)
- |intros 2;apply (bool_elim ? (a ≟ c1));simplify;intros
- [unfold;intros;cases (in_list_cons_case ???? H13)
- [rewrite > H14;rewrite > (p_eqb1 ??? H10);autobatch
- |apply H11;autobatch]
- |destruct]]]]]
-qed.
-
-lemma fresh_GV_subst_X_Var : ∀s,c,y.
- N_fresh X (GV (subst_X s c (Var y))) ∈ GV s →
- N_fresh X (GV (subst_X s c (Var y))) = c.
-intros;apply p_eqb1;
-apply (bool_elim ? (N_fresh X (GV (subst_X s c (Var y)))≟c));intro
-[reflexivity
-|lapply (p_eqb2 ??? H1);lapply (p_fresh ? (GV (subst_X s c (Var y))));
- lapply (GV_subst_X_Var s c y);
- elim Hletin1;cases (Hletin2 (N_fresh X (GV (subst_X s c (Var y)))));
- apply H3;apply in_list_filter_r
- [assumption
- |change in ⊢ (???%) with (¬false);apply eq_f;
- apply p_eqb4;intro;elim (p_eqb2 ??? H1);autobatch]]
-qed.
-
-lemma L_check_aux_complete :
- ∀F:xheight.∀M.LL F M → ∀n.S_len M ≤ n → L_check_aux F M (S n) = true.
-intros 3;elim H
-[reflexivity
-|simplify;simplify in H5;rewrite > (? : n = S (pred n))
- [rewrite > H2
- [rewrite > H4
- [reflexivity
- |(* H5 *) elim daemon]
- |(* H5 *) elim daemon]
- |(* H5 *) elim daemon]
-|simplify;simplify in H3;
- rewrite > (? : (F c s ≟ F (N_fresh X (GV (subst_X s c (Var (F c s)))))
- (subst_Y (subst_X s c (Var (F c s))) (F c s)
- (Par (N_fresh X (GV (subst_X s c (Var (F c s))))))))
- = true)
- [simplify;
- rewrite > (? : subst_Y (subst_X s c (Var (F c s))) (F c s)
- (Par (N_fresh X (GV (subst_X s c (Var (F c s)))))) =
- subst_X s c (Par (N_fresh X (GV (subst_X s c (Var (F c s)))))))
- [rewrite > (? : n = S (pred n))
- [rewrite > H2
- [reflexivity
- |autobatch
- |(* H3 *) elim daemon]
- |(* H3 *) elim daemon]
- |rewrite < subst_X_decompose
- [reflexivity
- |rewrite > (L_to_closed F)
- [autobatch
- |lapply (H1 c)
- [autobatch
- |intro;reflexivity]]
- |autobatch]]
- |rewrite < subst_X_decompose
- [rewrite > subst_X_fp
- [rewrite < (swap_left X c) in ⊢ (? ? (? ? ? (? ? % ?)) ?);
- autobatch
- |autobatch]
- |rewrite > (L_to_closed F)
- [autobatch
- |lapply (H1 c)
- [autobatch
- |intro;reflexivity]]
- |autobatch]]]
-qed.
-
-inductive typ : Type ≝
-| TPar : X → typ
-| Fun : typ → typ → typ.
-
-notation "hvbox(a break ▸ b)"
- left associative with precedence 50
-for @{ 'blacktriangleright $a $b }.
-interpretation "STT arrow type" 'blacktriangleright a b = (Fun a b).
-
-include "datatypes/constructors.ma".
-
-definition DOM : list (X × typ) → list X ≝ λC.map ?? (fst ??) C.
-
-inductive context : list (X × typ) → Prop ≝
-| ctx_nil : context []
-| ctx_cons : ∀x,t,C.x ∉ DOM C → context C → context (〈x,t〉::C).
-
-(* ▸ = \rtrif *)
-inductive typing (F:xheight): list (X × typ) → S_exp → typ → Prop ≝
-| t_axiom : ∀C,x,t.context C → 〈x,t〉 ∈ C → typing F C (Par x) t
-| t_App : ∀C,M,N,t,u.typing F C M (t ▸ u) → typing F C N t →
- typing F C (App M N) u
-| t_Lam : ∀C,x,M,t,u.x ∉ DOM C → typing F (〈x,t〉::C) M u →
- typing F C (Abs (F x M) (subst_X M x (Var (F x M)))) (t ▸ u).
-
-inductive typing2 (F:xheight): list (X × typ) → S_exp → typ → Prop ≝
-| t2_axiom : ∀C,x,t.context C → 〈x,t〉 ∈ C → typing2 F C (Par x) t
-| t2_App : ∀C,M,N,t,u.typing2 F C M (t ▸ u) → typing2 F C N t →
- typing2 F C (App M N) u
-| t2_Lam : ∀C,x1,M,t,u.
- (∀x2.x2 ∉ DOM C → (x2 ∈ GV M → x2 = x1) →
- typing2 F (〈x2,t〉::C) (subst_X M x1 (Par x2)) u) →
- typing2 F C (Abs (F x1 M) (subst_X M x1 (Var (F x1 M)))) (t ▸ u).
-
-notation > "C ⊢[F] M : t"
- non associative with precedence 30 for @{ 'typjudg F $C $M $t }.
-notation > "C ⊢ M : t"
- non associative with precedence 30 for @{ 'typjudg ? $C $M $t }.
-notation < "mstyle color #007f00 (hvbox(C maction (⊢) (⊢ \sub F) break M : break t))"
- non associative with precedence 30 for @{ 'typjudg $F $C $M $t }.
-interpretation "Fsub subtype judgement" 'typjudg F C M t = (typing F C M t).
-
-notation > "C ⊨[F] M : t"
- non associative with precedence 30 for @{ 'typjudg2 F $C $M $t }.
-notation > "C ⊨ M : t"
- non associative with precedence 30 for @{ 'typjudg2 ? $C $M $t }.
-notation < "mstyle color #007f00 (hvbox(C maction (⊨) (⊨ \sub F) break M : break t))"
- non associative with precedence 30 for @{ 'typjudg2 $F $C $M $t }.
-interpretation "Fsub strong subtype judgement" 'typjudg2 F C M t = (typing2 F C M t).
-
-lemma in_ctx_to_in_DOM : ∀x,t.∀C:list (X × typ).〈x,t〉 ∈ C → x ∈ DOM C.
-intros 3;elim C
-[elim (not_in_list_nil ?? H)
-|elim (in_list_cons_case ???? H1)
- [rewrite < H2;simplify;autobatch
- |cases a;simplify;autobatch]]
-qed.
-lemma in_DOM_to_in_ctx : ∀x,C.x ∈ DOM C → ∃t.〈x,t〉 ∈ C.
-intros 2;elim C
-[elim (not_in_list_nil X ? H)
-|elim a in H1;simplify in H1;elim (in_list_cons_case ???? H1)
- [rewrite > H2;autobatch
- |cases (H H2);autobatch]]
-qed.
-
-lemma incl_DOM : ∀l1,l2. l1 ⊆ l2 → DOM l1 ⊆ DOM l2.
-intros;unfold in H;unfold;intros;cases (in_DOM_to_in_ctx ?? H1);autobatch;
-qed.
-
-lemma typing2_weakening : ∀F,C,M,t.
- C ⊨[F] M : t → ∀D.context D → C ⊆ D → D ⊨[F] M : t.
-intros 5;elim H;try autobatch size=7;
-apply t2_Lam;intros;apply H2;
-[intro;autobatch
-|*:autobatch]
-qed.
-
-definition swap_list : ∀N:Nset.N → N → list N → list N ≝
- λN,a,b,l.map ?? (pi_swap ? a b) l.
-
-lemma in_list_swap : ∀N:Nset.∀x,l.x ∈ l → ∀a,b.swap N a b x ∈ swap_list N a b l.
-intros;elim H;simplify;autobatch;
-qed.
-
-definition ctx_swap_X : X → X → list (X × typ) → list (X × typ) ≝
- λx1,x2,C.map ?? (λp.
- match p with
- [pair x t ⇒ 〈pi_swap ? x1 x2 x,t〉]) C.
-
-lemma in_ctx_swap : ∀x,t,C.〈x,t〉 ∈ C → ∀a,b.〈swap ? a b x,t〉 ∈ ctx_swap_X a b C.
-intros;generalize in match H;elim C;
-[elim (not_in_list_nil ?? H1)
-|simplify;inversion H2;simplify;intros;destruct;simplify;autobatch]
-qed.
-
-lemma ctx_swap_X_swap_list :
- ∀C,x1,x2.DOM (ctx_swap_X x1 x2 C) = swap_list ? x1 x2 (DOM C).
-intros;elim C
-[reflexivity
-|cases a;simplify;autobatch]
-qed.
-
-lemma swap_list_inv : ∀N,x1,x2,l.swap_list N x1 x2 (swap_list N x1 x2 l) = l.
-intros;elim l;simplify;autobatch;
-qed.
-
-lemma context_eqv : ∀C.context C → ∀a,b.context (ctx_swap_X a b C).
-intros;elim H
-[simplify;autobatch
-|simplify;apply ctx_cons
- [intro;apply H1;rewrite > ctx_swap_X_swap_list in H4;
- rewrite < (swap_inv ? a b);
- rewrite < (swap_list_inv ? a b);autobatch
- |assumption]]
-qed.
-
-lemma typing_swap : ∀F:xheight.∀C,M,t,x1,x2.
- C ⊨[F] M : t → ctx_swap_X x1 x2 C ⊨[F] (pi_swap ? x1 x2)·M : t.
-intros;elim H
-[simplify;apply t2_axiom
- [autobatch
- |rewrite < eq_swap_pi;autobatch]
-|simplify;autobatch
-|simplify;rewrite > pi_lemma1;simplify;applyS t2_Lam;
- intros;rewrite < (swap_inv ? x1 x2 x);
- change in ⊢ (? ? ? (? ? ? %) ?) with (pi_swap X x1 x2 · Par (swap X x1 x2 x));
- rewrite < pi_lemma1;apply H2
- [intro;apply H3;rewrite < (swap_inv ? x1 x2 x);
- rewrite > ctx_swap_X_swap_list;autobatch
- |intro;rewrite > H4;autobatch]]
-qed.
-
-lemma typing_to_typing2 : ∀F:xheight.∀C,M,t.C ⊢[F] M : t → C ⊨[F] M : t.
-intros;elim H;try autobatch;
-apply t2_Lam;intros;
-rewrite > subst_X_fp
-[rewrite > (? : 〈x2,t1〉::l = ctx_swap_X c x2 (〈c,t1〉::l))
- [autobatch
- |simplify;rewrite < eq_swap_pi;rewrite > swap_left;
- rewrite < (? : l = ctx_swap_X c x2 l)
- [reflexivity
- |generalize in match H1;generalize in match H4;elim l 0
- [intros;reflexivity
- |intro;cases a;simplify;intros;
- rewrite < eq_swap_pi;rewrite > swap_other
- [rewrite < H6
- [reflexivity
- |*:intro;autobatch]
- |*:intro;autobatch]]]]
-|assumption]
-qed.
+1) dimostrare che GV di un term judgment (debole) è vuoto
+2) dimostrare che pi*T = T se GV(T) = []
+3) term judgment forte -> term judgment debole
+4) allora per 1+2 => term judgment equivariante (entrambi)
+5) 4) => term judgment debole
-lemma typing2_to_typing : ∀F:xheight.∀C,M,t.C ⊨[F] M : t → C ⊢[F] M : t.
-intros;elim H;try autobatch;
-generalize in match (p_fresh ? (c::DOM l@GV s));
-generalize in match (N_fresh ? (c::DOM l@GV s));
-intros (xn f_xn);
-lapply (H2 xn)
-[rewrite > subst_X_fp in Hletin
- [lapply (t_Lam ??????? Hletin)
- [intro;apply f_xn;autobatch
- |rewrite < subst_X_fp in Hletin1
- [rewrite > subst_X_merge in Hletin1
- [rewrite < (? : F c s = F xn (subst_X s c (Par xn))) in Hletin1
- [assumption
- |rewrite > subst_X_fp
- [rewrite < (swap_left ? c xn) in ⊢ (? ? ? (? ? % ?));
- rewrite > eq_swap_pi;autobatch]]]]]]]
-intro;elim f_xn;autobatch;
-qed.
\ No newline at end of file
+*)
\ No newline at end of file