1 include "basics/list.ma".
2 include "basics/types.ma".
6 ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ [].
7 #A;#l;#a; @; #H; ndestruct;
10 ntheorem append_nil: ∀A:Type.∀l:list A.l @ □ = l.
12 #a;#l1;#IH;nnormalize;//;
15 ntheorem associative_append: ∀A:Type[0].associative (list A) (append A).
18 ##|#a;#x1;#H;nnormalize;//]
21 ntheorem cons_append_commute:
22 ∀A:Type[0].∀l1,l2:list A.∀a:A.
23 a :: (l1 @ l2) = (a :: l1) @ l2.
27 nlemma append_cons: ∀A.∀a:A.∀l,l1. l@(a::l1)=(l@[a])@l1.
28 #A;#a;#l;#l1;nrewrite > (associative_append ????);//;
32 nlet rec nth A l d n on n ≝
36 | cons (x : A) _ ⇒ x ]
37 | S n' ⇒ nth A (tail ? l) d n'].
39 nlet rec map A B f l on l ≝
40 match l with [ nil ⇒ nil B | cons (x:A) tl ⇒ f x :: map A B f tl ].
42 nlet rec foldr (A,B:Type[0]) (f : A → B → B) (b:B) l on l ≝
43 match l with [ nil ⇒ b | cons (a:A) tl ⇒ f a (foldr A B f b tl) ].
45 ndefinition length ≝ λT:Type[0].λl:list T.foldr T nat (λx,c.S c) O l.
48 λT:Type[0].λl:list T.λp:T → bool.
50 (λx,l0.match (p x) with [ true => x::l0 | false => l0]) [] l.
52 ndefinition iota : nat → nat → list nat ≝
53 λn,m. nat_rect_Type0 (λ_.list ?) (nil ?) (λx,acc.cons ? (n+x) acc) m.
55 (* ### induction principle for functions visiting 2 lists in parallel *)
57 ∀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.
58 \ 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 →
59 (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 ?)) →
60 (∀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)) →
62 #T1 #T2 #l1 #l2 #P #Hl #Pnil #Pcons
63 generalize in match Hl; generalize in match l2;
66 normalize #t2 #tl2 #H destruct
67 |#t1 #tl1 #IH #l2 cases l2
68 [normalize #H destruct
69 |#t2 #tl2 #H @Pcons @IH normalize in H;destruct //]
73 lemma eq_map : ∀A,B,f,g,l. (∀x.f x
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 g x) →
\ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"
\ 6map
\ 5/a
\ 6 A B f l
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/list/map.fix(0,3,1)"
\ 6map
\ 5/a
\ 6 A B g l.
78 lemma le_length_filter : ∀A,l,p.
\ 5a href="cic:/matita/basics/list/length.fix(0,1,1)"
\ 6length
\ 5/a
\ 6 A (
\ 5a href="cic:/matita/basics/list/filter.def(2)"
\ 6filter
\ 5/a
\ 6 A p l)
\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"
\ 6≤
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/list/length.fix(0,1,1)"
\ 6length
\ 5/a
\ 6 A l.
79 #A #l #p elim l normalize
81 |#a #tl #IH cases (p a) normalize
82 [@
\ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"
\ 6le_S_S
\ 5/a
\ 6 //
88 lemma length_append : ∀A,l,m.
\ 5a href="cic:/matita/basics/list/length.fix(0,1,1)"
\ 6length
\ 5/a
\ 6 A (l
\ 5a title="append" href="cic:/fakeuri.def(1)"
\ 6@
\ 5/a
\ 6m)
\ 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 A l
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/list/length.fix(0,1,1)"
\ 6length
\ 5/a
\ 6 A m.
91 |#H #tl #IH normalize <IH //]
94 inductive in_list (A:Type[0]): A → (
\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A) → Prop ≝
95 | in_list_head : ∀ x,l.(in_list A x (x
\ 5a title="cons" href="cic:/fakeuri.def(1)"
\ 6:
\ 5/a
\ 6:l))
96 | 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)).
98 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 ≝
99 λ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.
101 notation "hvbox(a break ∉ b)" non associative with precedence 45
102 for @{ 'notmem $a $b }.
104 interpretation "list member" 'mem x l = (in_list ? x l).
105 interpretation "list not member" 'notmem x l = (Not (in_list ? x l)).
106 interpretation "list inclusion" 'subseteq l1 l2 = (incl ? l1 l2).
108 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].
109 (*intros.unfold.intro.inversion H
110 [intros;lapply (sym_eq ? ? ? H2);destruct Hletin
114 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) →
115 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.
116 (*intros;inversion H;intros
117 [destruct H2;left;reflexivity
118 |destruct H4;right;assumption]
121 axiom in_list_tail : ∀l,x,y.
122 \ 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.
123 (*intros 4;elim (in_list_cons_case ? ? ? ? H)
128 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.
129 (*intros;elim (in_list_cons_case ? ? ? ? H)
131 |elim (not_in_list_nil ? ? H1)]
134 axiom in_list_to_in_list_append_l:
135 ∀A.∀x:A.∀l1,l2.
\ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"
\ 6in_list
\ 5/a
\ 6 ? x l1 →
\ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"
\ 6in_list
\ 5/a
\ 6 ? x (l1
\ 5a title="append" href="cic:/fakeuri.def(1)"
\ 6@
\ 5/a
\ 6l2).
139 |apply in_list_cons;assumption
143 axiom in_list_to_in_list_append_r:
144 ∀A.∀x:A.∀l1,l2.
\ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"
\ 6in_list
\ 5/a
\ 6 ? x l2 →
\ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"
\ 6in_list
\ 5/a
\ 6 ? x (l1
\ 5a title="append" href="cic:/fakeuri.def(1)"
\ 6@
\ 5/a
\ 6l2).
148 |apply in_list_cons;apply H;assumption
152 lemma in_list_append_elim:
153 ∀A,x,l1,l2.
\ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"
\ 6in_list
\ 5/a
\ 6 A x (l1
\ 5a title="append" href="cic:/fakeuri.def(1)"
\ 6@
\ 5/a
\ 6l2) →
154 ∀P:Prop.(
\ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"
\ 6in_list
\ 5/a
\ 6 A x l1 → P) → (
\ 5a href="cic:/matita/cr/lambda/in_list.ind(1,0,1)"
\ 6in_list
\ 5/a
\ 6 A x l2 → P) → P.
156 [ #l2 #H #P #H1 #H2 @H2 @H
157 | #a0 #al #IH #l2 #H #P #H1 #H2 normalize in H; @(
\ 5a href="cic:/matita/cr/lambda/in_list_inv_ind.def(2)"
\ 6in_list_inv_ind
\ 5/a
\ 6 ? x … H)
158 [#a1 #al1 #e0 #e1 destruct /
\ 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\ 5/span
\ 6\ 5/span
\ 6/
159 |#a1 #a2 #al1 #H3 #H4 #e1 #e2 destruct @(IH l2) /
\ 5span class="autotactic"
\ 63
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/cr/lambda/in_list.con(0,2,1)"
\ 6in_list_cons
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
166 let rec mem (A:Type) (eq: A → A → bool) x (l: list A) on l ≝
172 | false ⇒ mem A eq x l'
176 naxiom mem_true_to_in_list :
178 (\forall x,y.equ x y = true \to x = y) \to
179 \forall x,l.mem A equ x l = true \to in_list A x l.
181 [simplify in H1;destruct H1
182 |simplify in H2;apply (bool_elim ? (equ x a))
183 [intro;rewrite > (H ? ? H3);apply in_list_head
184 |intro;rewrite > H3 in H2;simplify in H2;
185 apply in_list_cons;apply H1;assumption]]
188 naxiom in_list_to_mem_true :
190 (\forall x.equ x x = true) \to
191 \forall x,l.in_list A x l \to mem A equ x l = true.
193 [elim (not_in_list_nil ? ? H1)
195 [simplify;rewrite > H;reflexivity
196 |simplify;rewrite > H4;apply (bool_elim ? (equ a1 a2));intro;reflexivity]].
199 naxiom in_list_filter_to_p_true : \forall A,l,x,p.
200 in_list A x (filter A l p) \to p x = true.
202 [simplify in H;elim (not_in_list_nil ? ? H)
203 |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1;
205 [elim (in_list_cons_case ? ? ? ? H1)
206 [rewrite > H3;assumption
211 naxiom in_list_filter : \forall A,l,p,x.in_list A x (filter A l p) \to in_list A x l.
213 [simplify in H;elim (not_in_list_nil ? ? H)
214 |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1;
216 [elim (in_list_cons_case ? ? ? ? H1)
217 [rewrite > H3;apply in_list_head
218 |apply in_list_cons;apply H;assumption]
219 |apply in_list_cons;apply H;assumption]]
222 naxiom in_list_filter_r : \forall A,l,p,x.
223 in_list A x l \to p x = true \to in_list A x (filter A l p).
225 [elim (not_in_list_nil ? ? H)
226 |elim (in_list_cons_case ? ? ? ? H1)
227 [rewrite < H3;simplify;rewrite > H2;simplify;apply in_list_head
228 |simplify;apply (bool_elim ? (p a));intro;simplify;
229 [apply in_list_cons;apply H;assumption
230 |apply H;assumption]]]
233 naxiom incl_A_A: ∀T,A.incl T A A.
234 (*intros.unfold incl.intros.assumption.
237 naxiom incl_append_l : ∀T,A,B.incl T A (A @ B).
238 (*unfold incl; intros;autobatch.
241 naxiom incl_append_r : ∀T,A,B.incl T B (A @ B).
242 (*unfold incl; intros;autobatch.
245 naxiom incl_cons : ∀T,A,B,x.incl T A B → incl T (x::A) (x::B).
246 (*unfold incl; intros;elim (in_list_cons_case ? ? ? ? H1);autobatch.
252 record Nset : Type[1] ≝
254 (* carrier is specified as a coercion: when an object X of type Nset is
255 given, but something of type Type is expected, Matita will insert a
256 hidden coercion: the user sees "X", but really means "carrier X" *)
258 N_eqb : carrier → carrier →
\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"
\ 6bool
\ 5/a
\ 6;
259 p_eqb1 : ∀x,y.N_eqb 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;
260 p_eqb2 : ∀x,y.N_eqb 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,2,0)"
\ 6false
\ 5/a
\ 6 → x
\ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"
\ 6≠
\ 5/a
\ 6 y;
261 N_fresh :
\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 carrier → carrier;
262 p_fresh : ∀l.N_fresh l
\ 5a title="list not member" href="cic:/fakeuri.def(1)"
\ 6∉
\ 5/a
\ 6 l
266 ∀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.
267 #P * /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5/span
\ 6\ 5/span
\ 6/
270 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.
271 #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)) //
272 #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)
275 lemma p_eqb4 : ∀X,x,y.x
\ 5a title="leibnitz's non-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,2,0)"
\ 6false
\ 5/a
\ 6.
276 #X #x #y #H1 @(
\ 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)) //
277 #H2 cases H1 #H3 cases (H3 (
\ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"
\ 6p_eqb1
\ 5/a
\ 6 ??? H2))
280 axiom X :
\ 5a href="cic:/matita/cr/lambda/Nset.ind(1,0,0)"
\ 6Nset
\ 5/a
\ 6.
282 inductive pre_tm : Type[0] ≝
283 | Par :
\ 5a href="cic:/matita/cr/lambda/X.dec"
\ 6X
\ 5/a
\ 6 → pre_tm
284 | Var :
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 → pre_tm
285 | App : pre_tm → pre_tm → pre_tm
286 | Abs : pre_tm → pre_tm.
288 inductive tm_level :
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 →
\ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"
\ 6pre_tm
\ 5/a
\ 6 → Prop ≝
289 | tml_Par : ∀n,x.tm_level n (
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"
\ 6Par
\ 5/a
\ 6 x)
290 | tml_Var : ∀n,m.n
\ 5a title="natural 'greater than'" href="cic:/fakeuri.def(1)"
\ 6>
\ 5/a
\ 6 m → tm_level n (
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"
\ 6Var
\ 5/a
\ 6 m)
291 | tml_App : ∀n,M1,M2.tm_level n M1 → tm_level n M2 → tm_level n (
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"
\ 6App
\ 5/a
\ 6 M1 M2)
292 | tml_Abs : ∀n,M0.tm_level (
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n) M0 → tm_level n (
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"
\ 6Abs
\ 5/a
\ 6 M0).
294 record ext_tm (l:
\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6) : Type[0] ≝ {
295 tm_of_etm :>
\ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"
\ 6pre_tm
\ 5/a
\ 6;
296 etm_level :
\ 5a href="cic:/matita/cr/lambda/tm_level.ind(1,0,0)"
\ 6tm_level
\ 5/a
\ 6 l tm_of_etm
300 * we don't want to specify "N_eqb X" or "N_eqb Y" for the equality on X or Y,
301 * so we use a notation "a ? b" to hide the naming structure
302 * to type ?, write \equest.
304 notation > "hvbox(a break ≟ b)"
305 non associative with precedence 40
306 for @{ 'equiv ? $a $b }.
307 notation < "hvbox(a break maction (≟) (≟\sub t) b)"
308 non associative with precedence 40
309 for @{ 'equiv $t $a $b }.
310 interpretation "name decidable equality" 'equiv t a b = (N_eqb t a b).
312 (* valida solo se u è chiuso *)
313 let rec subst t x u on t :
\ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"
\ 6pre_tm
\ 5/a
\ 6 ≝
315 [ Par x2 ⇒ match x
\ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"
\ 6≟
\ 5/a
\ 6 x2 with
319 | App t1 t2 ⇒
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"
\ 6App
\ 5/a
\ 6 (subst t1 x u) (subst t2 x u)
320 | Abs t1 ⇒
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"
\ 6Abs
\ 5/a
\ 6 (subst t1 x u) ].
322 let rec nth A (xl:
\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A) n on xl ≝
324 [ nil ⇒
\ 5a href="cic:/matita/basics/types/option.con(0,1,1)"
\ 6None
\ 5/a
\ 6 A
325 | cons x0 xl0 ⇒ match n with
326 [ O ⇒
\ 5a href="cic:/matita/basics/types/option.con(0,2,1)"
\ 6Some
\ 5/a
\ 6 A x0
327 | S m ⇒ nth A xl0 m ] ].
329 (* it's necessary to specify Nset... unification hint? *)
330 let rec posn (A:
\ 5a href="cic:/matita/cr/lambda/Nset.ind(1,0,0)"
\ 6Nset
\ 5/a
\ 6) (xl:
\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A) x on xl ≝
332 [ nil ⇒
\ 5a href="cic:/matita/basics/types/option.con(0,1,1)"
\ 6None
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6
333 | cons x0 xl0 ⇒ match x
\ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"
\ 6≟
\ 5/a
\ 6 x0 with
334 [ true ⇒
\ 5a href="cic:/matita/basics/types/option.con(0,2,1)"
\ 6Some
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6
335 | false ⇒ match posn A xl0 x with
336 [ None ⇒
\ 5a href="cic:/matita/basics/types/option.con(0,1,1)"
\ 6None
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6
337 | Some n ⇒
\ 5a href="cic:/matita/basics/types/option.con(0,2,1)"
\ 6Some
\ 5/a
\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6 (
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n) ] ] ].
339 let rec vopen t xl k on t ≝
342 | Var n ⇒ match
\ 5a href="cic:/matita/cr/lambda/nth.fix(0,1,1)"
\ 6nth
\ 5/a
\ 6 ? xl (n
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6k) with
344 | Some x ⇒
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"
\ 6Par
\ 5/a
\ 6 x ]
345 | App t1 t2 ⇒
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"
\ 6App
\ 5/a
\ 6 (vopen t1 xl k) (vopen t2 xl k)
346 | Abs t1 ⇒
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"
\ 6Abs
\ 5/a
\ 6 (vopen t1 xl (
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 k)) ].
348 let rec vclose t xl k on t ≝
350 [ Par x0 ⇒ match
\ 5a href="cic:/matita/cr/lambda/posn.fix(0,1,3)"
\ 6posn
\ 5/a
\ 6 ? xl x0 with
352 | Some n ⇒
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"
\ 6Var
\ 5/a
\ 6 (n
\ 5a title="natural plus" href="cic:/fakeuri.def(1)"
\ 6+
\ 5/a
\ 6k) ]
354 | App t1 t2 ⇒
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"
\ 6App
\ 5/a
\ 6 (vclose t1 xl k) (vclose t2 xl k)
355 | Abs t1 ⇒
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"
\ 6Abs
\ 5/a
\ 6 (vclose t1 xl (
\ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 k)) ].
359 [ 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]
360 | Var _ ⇒
\ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6]
361 | App u v ⇒ GV u
\ 5a title="append" href="cic:/fakeuri.def(1)"
\ 6@
\ 5/a
\ 6 GV v
364 (* as above, fp_perm is a coercion
365 * but being a coercion to FunClass, a different syntax is required
366 * I'll fix this later *)
367 record fp (X:
\ 5a href="cic:/matita/cr/lambda/Nset.ind(1,0,0)"
\ 6Nset
\ 5/a
\ 6) : Type[0] ≝
370 fp_injective :
\ 5a href="cic:/matita/basics/relations/injective.def(1)"
\ 6injective
\ 5/a
\ 6 ?? fp_perm;
371 fp_surjective :
\ 5a href="cic:/matita/basics/relations/surjective.def(1)"
\ 6surjective
\ 5/a
\ 6 ?? fp_perm;
372 fp_finite :
\ 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 → fp_perm x
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 x
375 definition 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.
377 record fp_pre_tm : Type[0] ≝
379 fppt_perm :1>
\ 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.ind(1,0,0)"
\ 6pre_tm
\ 5/a
\ 6;
380 fppt_injective :
\ 5a href="cic:/matita/basics/relations/injective.def(1)"
\ 6injective
\ 5/a
\ 6 ?? fppt_perm;
381 fppt_surjective :
\ 5a href="cic:/matita/basics/relations/surjective.def(1)"
\ 6surjective
\ 5/a
\ 6 ?? fppt_perm
384 (*coercion fp_perm : ∀N:Nset.∀F:fp N.N → N ≝ fp_perm on _F:(fp N) to ? → ?.
385 coercion fppt_perm : ∀F:fp_pre_tm.pre_tm → pre_tm ≝ fppt_perm on _F:fp_pre_tm to ? → ?.*)
387 (* notation "p·x" right associative with precedence 60 for @{'middot $p $x}.
388 interpretation "apply fp" 'middot p x = (fp_perm ? p x).
389 interpretation "apply fppt" 'middot p x = (fppt_perm p x).*)
391 let rec mapX (p:
\ 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) t on t :
\ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"
\ 6pre_tm
\ 5/a
\ 6 ≝
393 [ Par x ⇒
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"
\ 6Par
\ 5/a
\ 6 (p x)
395 | App u v ⇒
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"
\ 6App
\ 5/a
\ 6 (mapX p u) (mapX p v)
396 | Abs u ⇒
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"
\ 6Abs
\ 5/a
\ 6 (mapX p u) ].
398 definition swap : ∀N:
\ 5a href="cic:/matita/cr/lambda/Nset.ind(1,0,0)"
\ 6Nset
\ 5/a
\ 6.N → N → N → N ≝
399 λN,u,v,x.match (x
\ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"
\ 6≟
\ 5/a
\ 6 u) with
401 |false ⇒ match (x
\ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"
\ 6≟
\ 5/a
\ 6 v) with
405 lemma Neqb_n_n : ∀N:
\ 5a href="cic:/matita/cr/lambda/Nset.ind(1,0,0)"
\ 6Nset
\ 5/a
\ 6.∀n:N.(n
\ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"
\ 6≟
\ 5/a
\ 6 n)
\ 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.
406 #N #n /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/cr/lambda/p_eqb3.def(4)"
\ 6p_eqb3
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
409 lemma swap_left : ∀N,x,y.(
\ 5a href="cic:/matita/cr/lambda/swap.def(3)"
\ 6swap
\ 5/a
\ 6 N x y x)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 y.
410 #N #x #y whd in ⊢ (??%?); >(
\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"
\ 6Neqb_n_n
\ 5/a
\ 6) //
413 lemma swap_right : ∀N,x,y.(
\ 5a href="cic:/matita/cr/lambda/swap.def(3)"
\ 6swap
\ 5/a
\ 6 N x y y)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 x.
414 #N #x #y whd in ⊢ (??%?); >(
\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"
\ 6Neqb_n_n
\ 5/a
\ 6) @(
\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"
\ 6bool_elim
\ 5/a
\ 6 ? (y
\ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"
\ 6≟
\ 5/a
\ 6 x))
415 normalize #H /
\ 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/
418 lemma swap_other : ∀N,x,y,z.(z
\ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"
\ 6≠
\ 5/a
\ 6 x) → (z
\ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"
\ 6≠
\ 5/a
\ 6 y) → (
\ 5a href="cic:/matita/cr/lambda/swap.def(3)"
\ 6swap
\ 5/a
\ 6 N x y z)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 z.
419 #N #x #y #z #H1 #H2 normalize >(
\ 5a href="cic:/matita/cr/lambda/p_eqb4.def(4)"
\ 6p_eqb4
\ 5/a
\ 6 … H1)
420 normalize >(
\ 5a href="cic:/matita/cr/lambda/p_eqb4.def(4)"
\ 6p_eqb4
\ 5/a
\ 6 … H2) %
423 lemma swap_inv : ∀N,u,v,x.(
\ 5a href="cic:/matita/cr/lambda/swap.def(3)"
\ 6swap
\ 5/a
\ 6 N u v (
\ 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.
424 #N #u #v #x normalize
425 @(
\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"
\ 6bool_elim
\ 5/a
\ 6 ? (x
\ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"
\ 6≟
\ 5/a
\ 6 u)) #H1 >H1 normalize
426 [normalize >
\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"
\ 6Neqb_n_n
\ 5/a
\ 6 normalize
427 @(
\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"
\ 6bool_elim
\ 5/a
\ 6 ? (v
\ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"
\ 6≟
\ 5/a
\ 6 u)) #H2 normalize
428 [>(
\ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"
\ 6p_eqb1
\ 5/a
\ 6 … H2) >(
\ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"
\ 6p_eqb1
\ 5/a
\ 6 … H1) %
429 |>(
\ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"
\ 6p_eqb1
\ 5/a
\ 6 … H1) %
431 |@(
\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"
\ 6bool_elim
\ 5/a
\ 6 ? (x
\ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"
\ 6≟
\ 5/a
\ 6 v)) #H2 normalize
432 [>
\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"
\ 6Neqb_n_n
\ 5/a
\ 6 normalize >(
\ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"
\ 6p_eqb1
\ 5/a
\ 6 … H2) %
438 lemma swap_inj : ∀N,u,v.
\ 5a href="cic:/matita/basics/relations/injective.def(1)"
\ 6injective
\ 5/a
\ 6 ?? (
\ 5a href="cic:/matita/cr/lambda/swap.def(3)"
\ 6swap
\ 5/a
\ 6 N u v).
439 #N #u #v #x #y normalize @(
\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"
\ 6bool_elim
\ 5/a
\ 6 ? (x
\ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"
\ 6≟
\ 5/a
\ 6 u)) normalize #H1
440 [@(
\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"
\ 6bool_elim
\ 5/a
\ 6 ? (y
\ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"
\ 6≟
\ 5/a
\ 6 u)) normalize #H2
441 [#H3 >(
\ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"
\ 6p_eqb1
\ 5/a
\ 6 … H2) /
\ 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/
442 |@(
\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"
\ 6bool_elim
\ 5/a
\ 6 ? (y
\ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"
\ 6≟
\ 5/a
\ 6 v)) normalize #H3
443 [>(
\ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"
\ 6p_eqb1
\ 5/a
\ 6 ??? H3) /
\ 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/
444 |#H4 cases (
\ 5a href="cic:/matita/cr/lambda/p_eqb2.fix(0,0,3)"
\ 6p_eqb2
\ 5/a
\ 6 ??? H3) #H5 cases (H5 ?) //
447 |@(
\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"
\ 6bool_elim
\ 5/a
\ 6 ? (y
\ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"
\ 6≟
\ 5/a
\ 6 u)) normalize #H2
448 [@(
\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"
\ 6bool_elim
\ 5/a
\ 6 ? (x
\ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"
\ 6≟
\ 5/a
\ 6 v)) normalize #H3 #H4
449 [>H4 in H1; #H1 >H1 in H3;#H3 destruct (H3)
450 |>H4 in H3; >
\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"
\ 6Neqb_n_n
\ 5/a
\ 6 #H5 destruct (H5)
452 |@(
\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"
\ 6bool_elim
\ 5/a
\ 6 ? (x
\ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"
\ 6≟
\ 5/a
\ 6 v)) normalize #H3
453 [@(
\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"
\ 6bool_elim
\ 5/a
\ 6 ? (y
\ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"
\ 6≟
\ 5/a
\ 6 v)) normalize #H4 #H5
454 [>(
\ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"
\ 6p_eqb1
\ 5/a
\ 6 … H4) /
\ 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/
455 |>H5 in H2; >
\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"
\ 6Neqb_n_n
\ 5/a
\ 6 #H2 destruct (H2)
457 |cases (y
\ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"
\ 6≟
\ 5/a
\ 6 v) normalize #H4
458 [>H4 in H1; >
\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"
\ 6Neqb_n_n
\ 5/a
\ 6 #H1 destruct (H1)
466 lemma swap_surj : ∀N,u,v.
\ 5a href="cic:/matita/basics/relations/surjective.def(1)"
\ 6surjective
\ 5/a
\ 6 ?? (
\ 5a href="cic:/matita/cr/lambda/swap.def(3)"
\ 6swap
\ 5/a
\ 6 N u v).
467 #N #u #v #z normalize @(
\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"
\ 6bool_elim
\ 5/a
\ 6 ? (z
\ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"
\ 6≟
\ 5/a
\ 6 v)); #H1
468 [%[@u] >
\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"
\ 6Neqb_n_n
\ 5/a
\ 6 normalize /
\ 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/
469 |@(
\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"
\ 6bool_elim
\ 5/a
\ 6 ? (z
\ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"
\ 6≟
\ 5/a
\ 6 u)) #H2
471 >(
\ 5a href="cic:/matita/cr/lambda/p_eqb4.def(4)"
\ 6p_eqb4
\ 5/a
\ 6 ? v u)
472 [>
\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"
\ 6Neqb_n_n
\ 5/a
\ 6 normalize /
\ 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/
473 |% #H3 cases (
\ 5a href="cic:/matita/cr/lambda/p_eqb2.fix(0,0,3)"
\ 6p_eqb2
\ 5/a
\ 6 ??? H1) /
\ 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/
481 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.
482 #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])]
483 #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/
486 definition pi_swap : ∀N,u,v.
\ 5a href="cic:/matita/cr/lambda/fp.ind(1,0,1)"
\ 6fp
\ 5/a
\ 6 N ≝
487 λN,u,v.
\ 5a href="cic:/matita/cr/lambda/fp.con(0,1,1)"
\ 6mk_fp
\ 5/a
\ 6 ? (
\ 5a href="cic:/matita/cr/lambda/swap.def(3)"
\ 6swap
\ 5/a
\ 6 N u v) (
\ 5a href="cic:/matita/cr/lambda/swap_inj.def(6)"
\ 6swap_inj
\ 5/a
\ 6 N u v) (
\ 5a href="cic:/matita/cr/lambda/swap_surj.def(6)"
\ 6swap_surj
\ 5/a
\ 6 N u v) (
\ 5a href="cic:/matita/cr/lambda/swap_finite.def(6)"
\ 6swap_finite
\ 5/a
\ 6 N u v).
489 lemma eq_swap_pi : ∀N,u,v,x.
\ 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 \ 5a href="cic:/matita/cr/lambda/pi_swap.def(7)"
\ 6pi_swap
\ 5/a
\ 6 N u v x.
494 ∀s,c,x.(x ∈ GV s → x = c) → subst_X s c (Par x) = (pi_swap ? c x)·s.
495 intros 3;elim s 0;simplify;intros
496 [rewrite < eq_swap_pi;apply (bool_elim ? (c ≟ c1));simplify;intro
497 [rewrite > (p_eqb1 ??? H1);autobatch
498 |apply (bool_elim ? (x ≟ c1));intro
499 [elim (p_eqb2 ??? H1);rewrite < H
501 |rewrite > (p_eqb1 ??? H2);autobatch]
502 |rewrite > swap_other;autobatch]]
507 |intro;apply H2;autobatch]
508 |intro;apply H2;autobatch]
514 lemma subst_x_x : ∀M,x.
\ 5a href="cic:/matita/cr/lambda/subst.fix(0,0,3)"
\ 6subst
\ 5/a
\ 6 M x (
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"
\ 6Par
\ 5/a
\ 6 x)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 M.
515 #M #x elim M normalize
516 [#x0 @(
\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"
\ 6bool_elim
\ 5/a
\ 6 ? (x
\ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"
\ 6≟
\ 5/a
\ 6 x0)) normalize #H1 /
\ 5span class="autotactic"
\ 63
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"
\ 6eq_f
\ 5/a
\ 6,
\ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"
\ 6p_eqb1
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
517 |*:/
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5/span
\ 6\ 5/span
\ 6/]
520 lemma pre_tm_inv_Par :
521 ∀P:
\ 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.ind(1,0,0)"
\ 6pre_tm
\ 5/a
\ 6 → Prop.
522 ∀x.(∀x0.P (
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"
\ 6Par
\ 5/a
\ 6 x) (
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"
\ 6Par
\ 5/a
\ 6 x0)) → ∀M.
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"
\ 6Par
\ 5/a
\ 6 x
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 M → P (
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"
\ 6Par
\ 5/a
\ 6 x) M.
525 |#n #H1 destruct (H1)
526 |#M1 #M2 #H1 destruct (H1)
527 |#M0 #H1 destruct (H1)
531 lemma pre_tm_inv_Var :
532 ∀P:
\ 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.ind(1,0,0)"
\ 6pre_tm
\ 5/a
\ 6 → Prop.
533 ∀n.(∀n0.P (
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"
\ 6Var
\ 5/a
\ 6 n) (
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"
\ 6Var
\ 5/a
\ 6 n0)) → ∀M.
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"
\ 6Var
\ 5/a
\ 6 n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 M → P (
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"
\ 6Var
\ 5/a
\ 6 n) M.
536 |#x #H1 destruct (H1)
537 |#M1 #M2 #H1 destruct (H1)
538 |#M0 #H1 destruct (H1)
542 lemma pre_tm_inv_Lam :
543 ∀P:
\ 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.ind(1,0,0)"
\ 6pre_tm
\ 5/a
\ 6 → Prop.
544 ∀M.(∀N0.P (
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"
\ 6Abs
\ 5/a
\ 6 M) (
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"
\ 6Abs
\ 5/a
\ 6 N0)) → ∀N.
\ 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 N → P (
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"
\ 6Abs
\ 5/a
\ 6 M) N.
547 |#x #H1 destruct (H1)
548 |#n #H1 destruct (H1)
549 |#M1 #M2 #H1 destruct (H1)
553 lemma pre_tm_inv_App :
554 ∀P:
\ 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.ind(1,0,0)"
\ 6pre_tm
\ 5/a
\ 6 → Prop.
555 ∀M1,M2.(∀N1,N2.P (
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"
\ 6App
\ 5/a
\ 6 M1 M2) (
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"
\ 6App
\ 5/a
\ 6 N1 N2)) →
556 ∀N.
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"
\ 6App
\ 5/a
\ 6 M1 M2
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 N → P (
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"
\ 6App
\ 5/a
\ 6 M1 M2) N.
557 #P #M1 #M2 #H #N cases N
559 |#x #H1 destruct (H1)
560 |#n #H1 destruct (H1)
561 |#M0 #H1 destruct (H1)
565 interpretation "permutation of pre_tm" 'middot p M = (mapX p M).
567 lemma Pi_Par_elim : ∀P:Prop.∀p.∀x,y.(∀z.y
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"
\ 6Par
\ 5/a
\ 6 z → P) →
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"
\ 6Par
\ 5/a
\ 6 x
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 p
\ 5a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"
\ 6·
\ 5/a
\ 6y → P.
569 [#x0 #H1 #H2 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5/span
\ 6\ 5/span
\ 6/
570 |#n #H1 #H2 normalize in H2; destruct (H2)
571 |#M1 #M2 #H1 #H2 normalize in H2; destruct (H2)
572 |#M0 #H1 #H2 normalize in H2; destruct (H2)
576 lemma Pi_Var_elim : ∀P:Prop.∀p,n,y.(∀n0.y
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"
\ 6Var
\ 5/a
\ 6 n0 → P) →
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"
\ 6Var
\ 5/a
\ 6 n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 p
\ 5a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"
\ 6·
\ 5/a
\ 6y → P.
578 [#x0 #H1 #H2 normalize in H2; destruct (H2)
579 |#n0 #H1 #H2 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5/span
\ 6\ 5/span
\ 6/
580 |#M1 #M2 #H1 #H2 normalize in H2; destruct (H2)
581 |#M0 #H1 #H2 normalize in H2; destruct (H2)
586 ∀P:Prop.∀p,M1,M2,y.(∀N1,N2.y
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"
\ 6App
\ 5/a
\ 6 N1 N2 → P) →
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"
\ 6App
\ 5/a
\ 6 M1 M2
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 p
\ 5a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"
\ 6·
\ 5/a
\ 6y → P.
587 #P #p #M1 #M2 #y cases y
588 [#x0 #H1 #H2 normalize in H2; destruct (H2)
589 |#n #H1 #H2 normalize in H2; destruct (H2)
590 |#M1 #M2 #H1 #H2 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5/span
\ 6\ 5/span
\ 6/
591 |#M0 #H1 #H2 normalize in H2; destruct (H2)
595 lemma Pi_Abs_elim : ∀P:Prop.∀p,M0,y.(∀N0.y
\ 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 N0 → P) →
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"
\ 6Abs
\ 5/a
\ 6 M0
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 p
\ 5a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"
\ 6·
\ 5/a
\ 6y → P.
597 [#x0 #H1 #H2 normalize in H2; destruct (H2)
598 |#n #H1 #H2 normalize in H2; destruct (H2)
599 |#M1 #M2 #H1 #H2 normalize in H2; destruct (H2)
600 |#M0 #H1 #H2 /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5/span
\ 6\ 5/span
\ 6/
605 ∀P:pre_tm → Prop.∀p,x,y.(∀z.P (p·z)) → p·x = y → P y.
608 definition fppt_of_fp :
\ 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 →
\ 5a href="cic:/matita/cr/lambda/fp_pre_tm.ind(1,0,0)"
\ 6fp_pre_tm
\ 5/a
\ 6.
609 #p @
\ 5a href="cic:/matita/cr/lambda/fp_pre_tm.con(0,1,0)"
\ 6mk_fp_pre_tm
\ 5/a
\ 6
610 [@(
\ 5a href="cic:/matita/cr/lambda/mapX.fix(0,1,3)"
\ 6mapX
\ 5/a
\ 6 p)
612 [#x0 #y #H1 @(
\ 5a href="cic:/matita/cr/lambda/Pi_Par_elim.def(4)"
\ 6Pi_Par_elim
\ 5/a
\ 6 … H1)
613 #z #H2 >H2 in H1; #H1 normalize in H1; destruct (H1) /
\ 5span class="autotactic"
\ 63
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"
\ 6eq_f
\ 5/a
\ 6,
\ 5a href="cic:/matita/cr/lambda/fp_injective.fix(0,1,3)"
\ 6fp_injective
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
614 |#n #y #H1 @(
\ 5a href="cic:/matita/cr/lambda/Pi_Var_elim.def(4)"
\ 6Pi_Var_elim
\ 5/a
\ 6 … H1)
615 #z #H2 >H2 in H1; #H1 @H1
616 |#M1 #M2 #IH1 #IH2 #y #H1 @(
\ 5a href="cic:/matita/cr/lambda/Pi_App_elim.def(4)"
\ 6Pi_App_elim
\ 5/a
\ 6 … H1)
617 #N1 #N2 #H2 >H2 in H1; #H1 normalize in H1; destruct (H1)
618 generalize in match e1; -e1 >e0 normalize in ⊢ (??%% → ?); #e1 /
\ 5span class="autotactic"
\ 63
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/eq_f2.def(3)"
\ 6eq_f2
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
619 |#M0 #IH0 #y #H1 @(
\ 5a href="cic:/matita/cr/lambda/Pi_Abs_elim.def(4)"
\ 6Pi_Abs_elim
\ 5/a
\ 6 … H1)
620 #N0 #H2 >H2 in H1; #H1 normalize in H1; destruct (H1) /
\ 5span class="autotactic"
\ 63
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"
\ 6eq_f
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
623 [#x0 cases (
\ 5a href="cic:/matita/cr/lambda/fp_surjective.fix(0,1,3)"
\ 6fp_surjective
\ 5/a
\ 6 ? p x0) #x1 #H1 %[@(
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,1,0)"
\ 6Par
\ 5/a
\ 6 x1)] >H1 %
624 |#n0 %[@(
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,2,0)"
\ 6Var
\ 5/a
\ 6 n0)] %
625 |#M1 #M2 * #N1 #IH1 * #N2 #IH2
626 %[@(
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,3,0)"
\ 6App
\ 5/a
\ 6 N1 N2)] /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/eq_f2.def(3)"
\ 6eq_f2
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
627 |#M0 * #N0 #IH0 %[@(
\ 5a href="cic:/matita/cr/lambda/pre_tm.con(0,4,0)"
\ 6Abs
\ 5/a
\ 6 N0)] /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"
\ 6eq_f
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
632 ∀M,P,x,pi.pi
\ 5a title="permutation of pre_tm" 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 x P)
\ 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 (pi
\ 5a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"
\ 6·
\ 5/a
\ 6 M) (pi x) (pi
\ 5a title="permutation of pre_tm" href="cic:/fakeuri.def(1)"
\ 6·
\ 5/a
\ 6 P).
634 [#c normalize @(
\ 5a href="cic:/matita/cr/lambda/bool_elim.def(1)"
\ 6bool_elim
\ 5/a
\ 6 ? (x
\ 5a title="name decidable equality" href="cic:/fakeuri.def(1)"
\ 6≟
\ 5/a
\ 6 c)) normalize #H1
635 [cut (pi x
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 pi c);
636 [/
\ 5span class="autotactic"
\ 63
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"
\ 6eq_f
\ 5/a
\ 6,
\ 5a href="cic:/matita/cr/lambda/p_eqb1.fix(0,0,3)"
\ 6p_eqb1
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
637 |#H2 >
\ 5a href="cic:/matita/cr/lambda/p_eqb3.def(4)"
\ 6p_eqb3
\ 5/a
\ 6 // ]
638 |cut (pi x
\ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"
\ 6≠
\ 5/a
\ 6 pi c)
639 [% #H2 >(
\ 5a href="cic:/matita/cr/lambda/fp_injective.fix(0,1,3)"
\ 6fp_injective
\ 5/a
\ 6 … H2) in H1; >
\ 5a href="cic:/matita/cr/lambda/Neqb_n_n.def(5)"
\ 6Neqb_n_n
\ 5/a
\ 6 #H1 destruct (H1)
640 |#H2 >
\ 5a href="cic:/matita/cr/lambda/p_eqb4.def(4)"
\ 6p_eqb4
\ 5/a
\ 6 // ]
647 ∀M,P,y,pi. pi · (subst_Y M y P) = subst_Y (pi · M) y (pi · P).
650 |simplify;apply (bool_elim ? (y ≟ c));simplify;intro;reflexivity
651 |simplify;autobatch paramodulation
652 |simplify;apply (bool_elim ? (y ≟ c));simplify;intro;autobatch paramodulation]
656 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).
658 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.
660 definition body ≝ λx,M.match M with
661 [ 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
664 inductive dupfree (A:Type[0]) :
\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A → Prop ≝
665 | df_nil : dupfree A
\ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6]
666 | 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:xl).
668 record df_list (A:Type[0]) : Type[0] ≝ {
669 list_of_dfl :>
\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 A;
670 dfl_dupfree :
\ 5a href="cic:/matita/cr/lambda/dupfree.ind(1,0,1)"
\ 6dupfree
\ 5/a
\ 6 A list_of_dfl
673 (* ciascuno dei pre_tm utilizzati nella costruzione deve essere un ext_tm 0 *)
674 inductive tm :
\ 5a href="cic:/matita/cr/lambda/pre_tm.ind(1,0,0)"
\ 6pre_tm
\ 5/a
\ 6 → Prop ≝
675 | 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))
676 | 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))
677 | 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:xl) 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)).
680 inductive tm2 : pre_tm → Prop ≝
681 | tm2_Par : ∀xl:df_list X.∀x.x ∈ xl → tm2 (Judg xl (Par x))
682 | tm2_App : ∀xl:df_list X.∀M1,M2.tm2 (Judg xl M1) → tm2 (Judg xl M2) → tm2 (Judg xl (App M1 M2))
683 | tm2_Lam : ∀xl:df_list X.∀M,C.(∀x.x ∉ xl@C → tm2 (Judg (x::xl) (body x M))) → tm2 (Judg xl (Abs M)).
688 inductive L (F:X → S_exp → Y) : S_exp → Prop \def
689 | LPar : ∀x:X.L F (Par x)
690 | LApp : ∀M,N:S_exp. (L F M) → (L F N) → L F (App M N)
691 | LAbs : ∀M:S_exp. ∀x:X. (L F M) →
692 L F (Abs (F x M) (subst_X M x (Var (F x M)))).
694 definition apartb : X → S_exp → bool ≝
695 λx,M.notb (mem X (N_eqb X) x (GV M)).
697 let rec E (x:X) (M:S_exp) on M : list Y ≝
701 | App u v ⇒ E x u @ E x v
702 | Abs y u ⇒ match apartb x u with
704 | false ⇒ y :: E x u ]].
706 definition apart : X → S_exp → Prop ≝
709 interpretation "name apartness wrt GV" 'apart x s = (apart x s).
711 lemma apartb_true_to_apart : ∀x,s.apartb x s = true → x # s.
713 lapply (in_list_to_mem_true ? (N_eqb X) ??? H1)
714 [simplify;intro;generalize in match (p_eqb2 ? x1 x1);
715 cases (x1 ≟ x1);intro;try autobatch;
717 |unfold apartb in H;rewrite > Hletin in H;simplify in H;destruct]
720 lemma apart_to_apartb_true : ∀x,s.x # s → apartb x s = true.
721 intros;cut (¬ (mem X (N_eqb X) x (GV s)) = true)
722 [unfold apartb;generalize in match Hcut;
723 cases (mem X (N_eqb X) x (GV s));intro;
726 |intro;apply H;autobatch]
729 lemma E_fresh : ∀x,M.x # M → E x M = [].
730 intros 2;elim M;simplify
735 |elim s1 in H2;simplify;
736 [simplify in H2;intro;apply H2;autobatch
738 |simplify in H4;intro;apply H4;autobatch
739 |simplify in H3;intro;apply H3;autobatch]]
740 |elim s in H2;simplify;
741 [simplify in H2;intro;apply H2;lapply (in_list_singleton_to_eq ??? H3);
744 |simplify in H4;intro;apply H4;autobatch
745 |simplify in H3;intro;apply H3;autobatch]]
747 [rewrite > (apart_to_apartb_true ?? H1);simplify;reflexivity
751 lemma mem_false_to_not_in_list :
752 ∀A,equ.(∀x,y.x = y → equ x y = true) →
753 ∀x,l.mem A equ x l = false → x ∉ l.
756 |intro;apply (bool_elim ? (equ x a));intros
757 [simplify in H2;rewrite > H4 in H2;simplify in H2;destruct
758 |cases (in_list_cons_case ???? H3)
763 [generalize in match H2;simplify;rewrite > H4;simplify;
768 lemma mem_append : ∀A,equ.
769 (∀x,y. x = y → equ x y = true) →
770 (∀x,y. equ x y = true → x = y) →
771 ∀x,l1,l2.mem A equ x (l1@l2) = orb (mem A equ x l1) (mem A equ x l2).
772 intros;apply (bool_elim ? (mem A equ x (l1@l2)));intro
774 [cases (in_list_append_to_or_in_list ???? Hcut)
775 [rewrite > in_list_to_mem_true
777 |intro;apply H;reflexivity
779 |cases (mem A equ x l1);simplify;try reflexivity;
780 rewrite > in_list_to_mem_true
782 |intro;apply H;reflexivity
785 |lapply (mem_false_to_not_in_list ????? H2)
787 |apply orb_elim;apply (bool_elim ? (mem A equ x l1));intro;simplify
788 [lapply (mem_true_to_in_list ????? H3);try assumption;
789 elim Hletin;autobatch
790 |apply (bool_elim ? (mem A equ x l2));intro;simplify
791 [lapply (mem_true_to_in_list ????? H4);try assumption;
792 elim Hletin;autobatch
796 (* lemma apartb_App_apart1 : ∀x,M,N.apartb x (App M N) = true → apartb x M = true.
797 simplify;intros;unfold apartb;
798 apply (bool_elim ? (mem X (N_eqb X) x (GV M)));
802 cut (x ∉ GV M @ GV N)
803 [cut (apartb x M = false → False)
804 [generalize in match Hcut1;cases (apartb x M);simplify;intro;
805 [reflexivity|elim H1;reflexivity]
809 lemma apartb_App_apart1 : ∀x,M,N.apartb x (App M N) = true → apartb x M = true.
811 lemma apartb_App_apart1 : ∀x,M,N.apartb x (App M N) = true → apartb x M = true.*)
813 axiom daemon : False.
815 lemma Ep : ∀x1,x2,M,Q.x1 ≠ x2 → x1 # Q → E x1 M = E x1 (subst_X M x2 Q).
817 [simplify;cases (x2 ≟ c);simplify;autobatch
820 |whd in ⊢ (??%?);rewrite > H2;
821 simplify in ⊢ (???%);
822 rewrite > (? : apartb x1 s = apartb x1 (subst_X s x2 Q))
825 [simplify;simplify in H2;apply (bool_elim ? (x1 ≟ c1));simplify;intro
826 [apply (bool_elim ? (x2 ≟ c1));simplify;intro
827 [lapply (p_eqb1 ??? H3);elim H;autobatch;
828 |rewrite > H3;reflexivity]
829 |apply (bool_elim ? (x2 ≟ c1));simplify;intro
831 |rewrite > H3;reflexivity]]
833 |simplify;rewrite > mem_append
834 [rewrite > mem_append
835 [unfold apartb in H3;unfold apartb in H4;autobatch paramodulation
841 lemma pi_Abs : ∀pi,x,M.pi · Abs x M = Abs x (pi · M).
845 lemma E_Abs : ∀x,y,v,M.y ∈ E x (Abs v M) → y ∈ v::E x M.
846 intros 4;simplify;cases (apartb x M);simplify;intro
847 [elim (not_in_list_nil ?? H)
851 lemma E_all_fresh : ∀x1,x2,x3,M.
852 x3 ≠ x1 → x3 ≠ x2 → E x3 M = E x3 (subst_X M x1 (Par x2)).
853 intros;elim M;simplify
854 [cases (x1 ≟ c);reflexivity
856 |autobatch paramodulation
857 |rewrite > (? : apartb x3 s = apartb x3 (subst_X s x1 (Par x2)))
858 [rewrite > H2;reflexivity
860 [simplify;simplify in H2;apply (bool_elim ? (x1 ≟ c1));simplify;intro
861 [lapply (p_eqb1 ??? H3);rewrite < Hletin;
862 rewrite > p_eqb4 [|assumption]
863 rewrite > p_eqb4 [|assumption]
867 |simplify;rewrite > mem_append
868 [rewrite > mem_append
869 [unfold apartb in H3;unfold apartb in H4;
870 autobatch paramodulation
876 lemma E_fresh_subst_Y :
877 ∀x1,x2,y,S.x1 ≠ x2 → E x1 S = E x1 (subst_Y S y (Par x2)).
880 |simplify;cases (y ≟ c);simplify;reflexivity
881 |simplify;autobatch paramodulation
882 |simplify;apply (bool_elim ? (y ≟ c));intro;simplify
884 |rewrite < H1;rewrite < (? : apartb x1 s = apartb x1 (subst_Y s y (Par x2)))
888 |cases (y ≟ c1);simplify
889 [rewrite > p_eqb4;autobatch
891 |rewrite > mem_append [|*:autobatch]
892 rewrite > mem_append [|*:autobatch]
893 unfold apartb in H3;unfold apartb in H4;
894 autobatch paramodulation
895 |cases (y ≟ c1); simplify
900 lemma subst_X_apart : ∀x,M,N. x # M → subst_X M x N = M.
903 [simplify;simplify in H;
906 |intro;apply H;autobatch]
908 |simplify;rewrite > H
911 |intro;apply H2;simplify;autobatch]
912 |intro;apply H2;simplify;autobatch]
918 lemma subst_Y_not_dangling : ∀y,M,N. y ∉ LV M → subst_Y M y N = M.
922 |simplify;simplify in H;
925 |intro;apply H;autobatch]
926 |simplify;rewrite > H
929 |intro;apply H2;simplify;autobatch]
930 |intro;apply H2;simplify;autobatch]
931 |simplify;simplify in H1;apply (bool_elim ? (y ≟ c));simplify;intro
935 |intro;apply H1;apply in_list_filter_r;autobatch]]]
938 lemma subst_X_lemma :
939 ∀x1,x2,M,P,Q.x1 ≠ x2 → x1 # Q →
940 subst_X (subst_X M x1 P) x2 Q = subst_X (subst_X M x2 Q) x1 (subst_X P x2 Q).
942 [simplify;apply (bool_elim ? (x1 ≟ c));simplify;intro
944 [simplify;rewrite > H2;reflexivity
946 |apply (bool_elim ? (x2 ≟ c));simplify;intro
947 [rewrite > subst_X_apart;autobatch
948 |rewrite > H2;reflexivity]]
950 |*:simplify;autobatch paramodulation]
953 lemma subst_cancel : ∀x,y,M.x # M → M = subst_X (subst_Y M y (Par x)) x (Var y).
955 [simplify;simplify in H;rewrite > p_eqb4
958 |simplify;apply (bool_elim ? (y ≟ c));simplify;intro
959 [rewrite > p_eqb3 [|reflexivity]
960 simplify;rewrite > (p_eqb1 ??? H1);reflexivity
962 |simplify;simplify in H2;rewrite < H;
965 |intro;apply H2;autobatch]
966 |intro; apply H2;autobatch]
967 |simplify;simplify in H1;apply (bool_elim ? (y ≟ c));
969 [rewrite > subst_X_apart
977 lemma subst_X_merge : ∀M,N,x1,x2.x2 # M →
978 subst_X (subst_X M x1 (Par x2)) x2 N = subst_X M x1 N.
980 [simplify;apply (bool_elim ? (x1 ≟ c));simplify;intro
981 [rewrite > Neqb_n_n;reflexivity
984 |intro;elim H;simplify;autobatch]]
986 |simplify;simplify in H2;rewrite > H
991 |simplify;rewrite > H
996 lemma subst_X_Y_commute : ∀x1,x2,y,M,N. x1 ≠ x2 → y ∉ LV N →
997 subst_Y (subst_X M x1 N) y (Par x2) = subst_X (subst_Y M y (Par x2)) x1 N.
999 [simplify;apply (bool_elim ? (x1 ≟ c));simplify;intro
1000 [rewrite > subst_Y_not_dangling;autobatch
1002 |simplify;apply (bool_elim ? (y ≟ c));simplify;intro
1007 |simplify;autobatch paramodulation
1008 |simplify;apply (bool_elim ? (y ≟ c));simplify;intro
1010 |rewrite < H2;reflexivity]]
1013 inductive LL (F : X → S_exp → Y) : S_exp → Prop ≝
1014 | LLPar : ∀x.LL F (Par x)
1015 | LLApp : ∀M,N.LL F M → LL F N → LL F (App M N)
1016 | LLAbs : ∀x1,M.(∀x2.(x2 ∈ GV M → x2 = x1) → LL F (subst_X M x1 (Par x2))) →
1017 LL F (Abs (F x1 M) (subst_X M x1 (Var (F x1 M)))).
1019 include "nat/compare.ma".
1021 definition max : nat → nat → nat ≝
1022 λx,y.match leb x y with
1026 let rec S_len M ≝ match M with
1029 | App N P ⇒ S (max (S_len N) (S_len P))
1030 | Abs x N ⇒ S (S_len N) ].
1034 (∀M.(∀N.S_len N < S_len M → P N) → P M)
1037 cut (∀N.S_len N ≤ S_len M → P N)
1038 [|elim M 0;simplify;intros
1039 [1,2:apply H;intros;elim (not_le_Sn_O (S_len N1));autobatch
1040 |apply H;intros;generalize in match (trans_le ??? H4 H3);unfold max;
1041 apply (bool_elim ? (leb (S_len s) (S_len s1)));simplify;intros;autobatch
1042 |apply H;intros;apply H1;apply le_S_S_to_le;autobatch]]
1043 apply H;intros;autobatch;
1046 record height : Type ≝
1049 HE : ∀M:S_exp. ∀x:X. ∀pi:Pi. (L H M) → H x M = H (pi x) (pi · M);
1050 HF : ∀M:S_exp. ∀x:X. (L H M) → H x M ∉ E x M;
1051 HP : ∀M,Q:S_exp. ∀x1,x2:X. (L H M) → (L H Q) → (x1 ≟ x2) = false →
1052 apartb x1 Q = true → (H x1 M ≟ H x1 (subst_X M x2 Q)) = true
1056 record xheight : Type ≝
1059 XHE : ∀M:S_exp. ∀x:X. ∀pi:Pi. XH x M = XH (pi x) (pi · M);
1060 XHF : ∀M:S_exp. ∀x:X. XH x M ∉ E x M;
1061 XHP : ∀M,Q:S_exp. ∀x1,x2:X.(x1 ≟ x2) = false →
1062 apartb x1 Q = true → (XH x1 M ≟ XH x1 (subst_X M x2 Q)) = true
1066 include "logic/coimplication.ma".
1068 definition coincl : ∀A.list A → list A → Prop ≝ λA,l1,l2.∀x.x ∈ l1 ↔ x ∈ l2.
1070 notation > "hvbox(a break ≡ b)"
1071 non associative with precedence 45
1072 for @{'equiv $a $b}.
1074 notation < "hvbox(term 46 a break ≡ term 46 b)"
1075 non associative with precedence 45
1076 for @{'equiv $a $b}.
1078 interpretation "list coinclusion" 'equiv x y = (coincl ? x y).
1080 lemma refl_coincl : ∀A.∀l:list A.l ≡ l.
1081 intros;intro;split;intro;assumption;
1084 lemma filter_append : ∀A,l1,l2,p.filter A (l1@l2) p = filter A l1 p @ filter A l2 p.
1087 |simplify;cases (p a);simplify;rewrite < H;reflexivity]
1090 lemma GV_subst_X_Var :
1091 ∀M,x,y. GV (subst_X M x (Var y)) ≡ filter ? (GV M) (λz.¬(x ≟ z)).
1092 intros;elim M;simplify
1093 [cases (x ≟ c);simplify;autobatch
1096 [rewrite > filter_append;cases (in_list_append_to_or_in_list ???? H2)
1097 [cases (H x1);autobatch
1098 |cases (H1 x1);autobatch]
1099 |rewrite > filter_append in H2;cases (in_list_append_to_or_in_list ???? H2)
1100 [cases (H x1);autobatch
1101 |cases (H1 x1);autobatch]]
1102 |intro;split;intro;cases (H x1);autobatch]
1105 lemma swap_GV : ∀x,M. x ∈ GV M → ∀x1,x2.swap X x1 x2 x ∈ GV (pi_swap X x1 x2 · M).
1107 [simplify;simplify in H;rewrite > (in_list_singleton_to_eq ??? H);autobatch
1108 |simplify in H;elim (not_in_list_nil ?? H)
1109 |simplify in H2;simplify;cases (in_list_append_to_or_in_list ???? H2);autobatch
1110 |simplify in H1;simplify;autobatch]
1113 (* easy to prove, but not needed *)
1114 lemma L_swap : ∀F:xheight.∀M.L F M →
1115 ∀x1,x2.L F (pi_swap ? x1 x2 · M).
1119 |simplify;rewrite > pi_lemma1;simplify;
1120 rewrite > (?: F c s = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s))
1121 [apply LAbs;assumption
1125 lemma LL_swap : ∀F:xheight.∀M.LL F M →
1126 ∀x1,x2.LL F (pi_swap ? x1 x2 · M).
1130 |simplify;rewrite > pi_lemma1;simplify;
1131 rewrite > (?: F c s = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s))
1132 [apply LLAbs;intros;lapply (H2 (pi_swap ? x1 x2 x))
1133 [rewrite > (?: Par x = pi_swap ? x1 x2 · (Par (pi_swap ? x1 x2 x)))
1135 |elim daemon (*involution*)]
1136 |intro;rewrite < (swap_inv ? x1 x2 c);
1137 rewrite < eq_swap_pi;apply eq_f;rewrite > eq_swap_pi;apply H3;
1138 rewrite < (swap_inv ? x1 x2 x);autobatch]
1142 (*lemma LL_subst_X : ∀F:xheight.∀M.LL F M →
1143 ∀x1,x2.LL F (subst_X M x1 (Par x2)).
1144 intros 2;apply (S_len_ind ?? M);intro;cases M1;simplify;intros
1145 [cases (x1 ≟ c);simplify;autobatch
1146 |inversion H1;simplify;intros;destruct
1147 |inversion H1;simplify;intros;destruct;
1148 clear H3 H5;apply LLApp;apply H;try assumption
1149 [(* len *)elim daemon
1150 |(* len *)elim daemon]
1151 |inversion H1;simplify;intros;destruct;
1152 unfold lam in H4;clear H3;destruct;
1153 apply (bool_elim ? (x1 ≟ c1));intro
1154 [rewrite > subst_X_apart
1156 |intro;rewrite > (?: (x1 ≟ c1) = false) in H3
1158 |elim (GV_subst_X_Var s1 c1 (F c1 s1) x1);
1159 lapply (H5 H4);lapply (in_list_filter_to_p_true ???? Hletin);
1160 apply p_eqb4;intro;rewrite > H7 in Hletin1;
1161 rewrite > Neqb_n_n in Hletin1;simplify in Hletin1;destruct]]
1162 |letin c2 ≝ (N_fresh ? (x1::x2::c1::GV s1));
1163 cut (c2 ∉ (x1::x2::c1::GV s1)) as Hc2 [|apply p_fresh]
1165 rewrite > (? : s1 = subst_X (subst_X s1 c1 (Par c2)) c2 (Par c1)) in ⊢ (? ? (? ? (? (? % ? ?) ? ?)))
1166 [|rewrite > subst_X_merge
1168 |intro;apply Hc2;autobatch depth=4]]
1169 rewrite > (? : F c1 s1 = F c2 (subst_X s1 c1 (Par c2)))
1170 [|rewrite > subst_X_fp
1171 [rewrite < (swap_left ? c1 c2) in ⊢ (? ? ? (? ? % ?));
1172 rewrite > eq_swap_pi;autobatch
1173 |intro;elim Hc2;autobatch depth=4]]
1174 rewrite > subst_X_merge
1175 [|intro;apply Hc2;do 2 apply in_list_cons;generalize in match H4;
1176 elim s1 0;simplify;intros
1177 [apply (bool_elim ? (c1 ≟ c));intro;
1178 rewrite > H6 in H5;simplify in H5;
1179 lapply (in_list_singleton_to_eq ??? H5)
1180 [rewrite > Hletin;autobatch
1181 |rewrite > Hletin in H6;rewrite > Neqb_n_n in H6;destruct]
1182 |elim (not_in_list_nil ?? H5)
1183 |cases (in_list_append_to_or_in_list ???? H7)
1184 [cases (in_list_cons_case ???? (H5 H8));autobatch
1185 |cases (in_list_cons_case ???? (H6 H8));autobatch]
1187 rewrite > (subst_X_lemma c2 x1 ? ??)
1188 [simplify;rewrite > (? : F c2 (subst_X s1 c1 (Par c2)) = F c2 (subst_X (subst_X s1 c1 (Par c2)) x1 (Par x2)))
1189 [|apply p_eqb1;apply XHP;
1190 [apply p_eqb4;intro;apply Hc2;autobatch
1191 |simplify;rewrite > (? : (c2 ≟ x2) = false)
1193 |apply p_eqb4;intro;apply Hc2;autobatch]]]
1201 |apply H2;intro;elim Hc2;autobatch depth=4]]
1202 |intro;apply Hc2;autobatch
1203 |simplify;intro;elim Hc2;rewrite > (? : c2 = x2);autobatch]]]
1206 lemma L_to_LL : ∀M.∀F:xheight.L F M → LL F M.
1210 |apply LLAbs;intros;rewrite > subst_X_fp;autobatch]
1213 lemma LL_to_L : ∀M.∀F:xheight.LL F M → L F M.
1216 |apply LAbs;lapply (H2 c)
1217 [rewrite > subst_X_x_x in Hletin;assumption
1218 |intro;reflexivity]]
1221 lemma subst_X_decompose :
1222 ∀x,y,M,N.y ∉ LV M → y ∉ E x M →
1223 subst_X M x N = subst_Y (subst_X M x (Var y)) y N.
1225 [simplify;cases (x ≟ c);simplify;
1226 [rewrite > p_eqb3;autobatch
1228 |simplify;simplify in H;
1231 |intro;apply H;autobatch]
1232 |simplify;rewrite < H
1235 |intro;apply H2;simplify;autobatch
1236 |intro;apply H3;simplify;autobatch]
1237 |intro;apply H2;simplify;autobatch
1238 |intro;apply H3;simplify;autobatch]
1239 |simplify;apply (bool_elim ? (y ≟ c));intros;
1240 [simplify;apply (bool_elim ? (apartb x s))
1242 lapply (apartb_true_to_apart ?? H4);
1243 rewrite > subst_X_apart
1244 [rewrite > subst_X_apart
1248 |intro;simplify in H2;rewrite > H4 in H2;
1249 simplify in H2;elim H2;
1250 rewrite > (p_eqb1 ??? H3);autobatch]
1251 |simplify;rewrite < H;
1253 |generalize in match H1;simplify;elim (LV s)
1255 |intro;cases (in_list_cons_case ???? H6)
1256 [elim H5;simplify;rewrite < H7;rewrite > H3;simplify;autobatch
1257 |elim (H4 ? H7);intro;apply H5;simplify;cases (¬ (a ≟ c));simplify;autobatch]]
1258 |intro;apply H2;simplify;apply (bool_elim ? (apartb x s));intro
1259 [simplify;rewrite > E_fresh in H4
1262 |simplify;autobatch]]]]
1265 lemma subst_Y_decompose :
1267 subst_Y M y N = subst_X (subst_Y M y (Par x)) x N.
1269 [simplify;simplify in H;rewrite > p_eqb4
1271 |intro;apply H;autobatch]
1272 |simplify;apply (bool_elim ? (y ≟ c));simplify;intro
1273 [rewrite > Neqb_n_n;reflexivity
1275 |simplify;rewrite < H
1278 |intro;apply H2;simplify;autobatch]
1279 |intro;apply H2;simplify;autobatch]
1280 |simplify;simplify in H1;apply (bool_elim ? (y ≟ c));simplify;intro
1281 [simplify;rewrite > subst_X_apart
1289 lemma pre_height : ∀x1,x2,y,M.y ∉ E x1 M → y ∉ LV M →
1290 subst_X M x1 (Par x2) = subst_Y (subst_X M x1 (Var y)) y (Par x2).
1291 intros;apply subst_X_decompose;assumption;
1294 lemma HL_conv : ∀x,y,M.y ∈ E x M → M ≠ subst_Y (subst_X M x (Var y)) y (Par x).
1296 [simplify in H;elim (not_in_list_nil ?? H);
1297 |simplify in H;elim (not_in_list_nil ?? H)
1298 |simplify;intro;simplify in H2;destruct;
1299 cases (in_list_append_to_or_in_list ???? H2);autobatch
1300 |simplify;simplify in H1;
1301 cut (apartb x s = false)
1302 [rewrite > Hcut in H1;simplify in H1;apply (bool_elim ? (y ≟ c));intro
1303 [simplify;intro;cut (¬ x # s)
1304 [apply Hcut1;generalize in match H3;elim s 0;simplify;
1305 [intro;apply (bool_elim ? (x ≟ c1));simplify;intros;
1309 |intros;destruct;intro;cases (in_list_append_to_or_in_list ???? H3)
1316 |intros;destruct;apply H4;demodulate all]
1317 |intro;rewrite > (apart_to_apartb_true ?? H4) in Hcut;destruct]
1318 |simplify;intro;apply H
1319 [cases (in_list_cons_case ???? H1)
1320 [rewrite > p_eqb3 in H2
1324 |destruct;assumption]]
1325 |generalize in match H1;cases (apartb x s);simplify;intro
1326 [elim (not_in_list_nil ?? H2)
1330 let rec BV t ≝ match t with
1333 | App t1 t2 ⇒ BV t1 @ BV t2
1334 | Abs y u ⇒ y::BV u ].
1336 lemma E_BV : ∀x,M.E x M ⊆ BV M.
1337 intros;elim M;simplify
1338 [1,2:unfold;intros;assumption
1339 |unfold;intros;cases (in_list_append_to_or_in_list ???? H2);autobatch
1340 |cases (apartb x s);simplify
1341 [unfold;intros;elim (not_in_list_nil ?? H1)
1346 let rec L_check (F:xheight) M on M ≝ match M with
1349 | App N P ⇒ andb (L_check F N) (L_check F P)
1350 | Abs y N ⇒ let X ≝ (N_fresh ? (GV M)) in
1351 andb (y ≟ F X (subst_Y N y (Par X)))
1352 (L_check F (subst_Y N y (Par X))) ].
1355 let rec L_check_aux (F:xheight) M n on n ≝ match n with
1356 [ O ⇒ false (* vacuous *)
1357 | S m ⇒ match M with
1360 | App N P ⇒ andb (L_check_aux F N m) (L_check_aux F P m)
1361 | Abs y N ⇒ let X ≝ (N_fresh ? (GV M)) in
1362 andb (y ≟ F X (subst_Y N y (Par X)))
1363 (L_check_aux F (subst_Y N y (Par X)) m) ]].
1365 lemma L_check_aux_sound :
1366 ∀F,M,n.S_len M ≤ n → L_check_aux F M (S n) = true → L F M.
1367 intros 2;apply (S_len_ind ?? M);intro;cases M1;intros
1369 |simplify in H2;destruct
1370 |simplify in H2;generalize in match H2;
1371 apply (andb_elim (L_check_aux F s n) (L_check_aux F s1 n));
1372 apply (bool_elim ? (L_check_aux F s n));simplify;intros
1374 [apply (H ?? (pred n))
1375 [simplify;(*len*)elim daemon
1376 |simplify in H1;generalize in match H1;cases n;intros
1377 [elim (not_le_Sn_O ? H5)
1378 |simplify;elim daemon (* H5 *)]
1379 |(* H3 *) elim daemon]
1380 |apply (H ?? (pred n))
1381 [simplify;(*len*) elim daemon
1382 |simplify in H1;generalize in match H1;cases n;intros
1383 [elim (not_le_Sn_O ? H5)
1384 |simplify;elim daemon (* H5 *)]
1385 |(* H4 *) elim daemon]]
1387 |simplify in H2;generalize in match H2;clear H2;
1388 apply (andb_elim (c ≟ F (N_fresh X (GV s)) (subst_Y s c (Par (N_fresh X (GV s)))))
1389 (L_check_aux F (subst_Y s c (Par (N_fresh X (GV s)))) n));
1390 apply (bool_elim ? (c≟F (N_fresh X (GV s)) (subst_Y s c (Par (N_fresh X (GV s))))));
1392 [rewrite > (p_eqb1 ??? H2);
1396 (Par (N_fresh X (GV s))))
1398 (Var (F (N_fresh X (GV s)) (subst_Y s c (Par (N_fresh X (GV s)))))))
1400 [apply LAbs;apply (H ?? (pred n))
1401 [simplify;(*len*)elim daemon
1402 |simplify in H1;generalize in match H1;cases n;intros
1403 [elim (not_le_Sn_O ? H4)
1404 |simplify;elim daemon (* H4 *)]
1405 |rewrite > (? : S (pred n) = n)
1407 |(*arith*)elim daemon]]
1408 |rewrite < subst_Y_decompose
1409 [rewrite < (p_eqb1 ??? H2);autobatch
1414 lemma LV_subst_X : ∀s,x,y. LV (subst_X s x (Var y)) ⊆ y::LV s.
1416 [simplify;cases (x ≟ c);simplify;
1418 |unfold;intros;elim (not_in_list_nil ?? H)]
1419 |simplify;unfold;intros;autobatch
1420 |simplify;unfold;intros;
1421 cases (in_list_append_to_or_in_list ???? H2)
1422 [lapply (H ? H3);autobatch
1423 |lapply (H1 ? H3);cases (in_list_cons_case ???? Hletin)
1424 [applyS in_list_head
1426 |simplify;unfold;intros;
1427 lapply (in_list_filter ???? H1);
1428 lapply (H ? Hletin);
1429 cases (in_list_cons_case ???? Hletin1)
1430 [rewrite > H2;autobatch
1431 |apply in_list_cons;apply in_list_filter_r
1433 |apply (in_list_filter_to_p_true ???? H1)]]]
1436 lemma eq_list_nil : ∀A.∀l:list A.(∀x.x ∉ l) → l = [].
1437 intros 2;cases l;intro
1439 |elim (H a);autobatch]
1443 lemma L_to_closed : ∀F:xheight.∀M.L F M → LV M = [].
1446 |simplify;autobatch paramodulation
1447 |simplify;generalize in match H2;generalize in match (F c s);elim s
1448 [simplify;apply (bool_elim ? (c ≟ c1));simplify;intro
1449 [rewrite > p_eqb3;reflexivity
1451 |simplify in H3;destruct
1452 |simplify in H5;simplify;
1454 filter Y (LV (subst_X s1 c (Var c1))@LV (subst_X s2 c (Var c1))) (λz.¬(z≟c1)) =
1455 filter Y (LV (subst_X s1 c (Var c1))) (λz.¬(z≟c1))@ filter Y (LV (subst_X s2 c (Var c1))) (λz.¬(z≟c1)))
1459 |generalize in match H5;cases (LV s2);simplify;
1461 |cases (LV s1);simplify;intro;destruct]]
1462 |generalize in match H5;cases (LV s1);simplify;intro
1465 |elim (LV (subst_X s1 c (Var c1)));simplify
1467 |cases (a ≟ c1);simplify;rewrite > H6;reflexivity]]
1468 |simplify;apply eq_list_nil;intro;intro;
1469 lapply (in_list_filter ???? H5) as H6;
1470 lapply (in_list_filter ???? H6) as H7;
1471 lapply (in_list_filter_to_p_true ???? H5) as H8;
1472 lapply (in_list_filter_to_p_true ???? H6) as H9;
1473 lapply (LV_subst_X ???? H7);
1475 [cases (in_list_cons_case ???? Hletin)
1476 [rewrite > (p_eqb3 ??? H10) in H8;simplify in H8;destruct
1477 |lapply (Hcut ? H10);lapply (in_list_singleton_to_eq ??? Hletin1);
1478 rewrite > (p_eqb3 ??? Hletin2) in H9;simplify in H9;destruct]
1479 |simplify in H4;generalize in match H4;elim (LV s1) 0;simplify
1480 [intro;unfold;intros;elim (not_in_list_nil ?? H11)
1481 |intros 2;apply (bool_elim ? (a ≟ c1));simplify;intros
1482 [unfold;intros;cases (in_list_cons_case ???? H13)
1483 [rewrite > H14;rewrite > (p_eqb1 ??? H10);autobatch
1484 |apply H11;autobatch]
1488 lemma fresh_GV_subst_X_Var : ∀s,c,y.
1489 N_fresh X (GV (subst_X s c (Var y))) ∈ GV s →
1490 N_fresh X (GV (subst_X s c (Var y))) = c.
1491 intros;apply p_eqb1;
1492 apply (bool_elim ? (N_fresh X (GV (subst_X s c (Var y)))≟c));intro
1494 |lapply (p_eqb2 ??? H1);lapply (p_fresh ? (GV (subst_X s c (Var y))));
1495 lapply (GV_subst_X_Var s c y);
1496 elim Hletin1;cases (Hletin2 (N_fresh X (GV (subst_X s c (Var y)))));
1497 apply H3;apply in_list_filter_r
1499 |change in ⊢ (???%) with (¬false);apply eq_f;
1500 apply p_eqb4;intro;elim (p_eqb2 ??? H1);autobatch]]
1503 lemma L_check_aux_complete :
1504 ∀F:xheight.∀M.LL F M → ∀n.S_len M ≤ n → L_check_aux F M (S n) = true.
1507 |simplify;simplify in H5;rewrite > (? : n = S (pred n))
1511 |(* H5 *) elim daemon]
1512 |(* H5 *) elim daemon]
1513 |(* H5 *) elim daemon]
1514 |simplify;simplify in H3;
1515 rewrite > (? : (F c s ≟ F (N_fresh X (GV (subst_X s c (Var (F c s)))))
1516 (subst_Y (subst_X s c (Var (F c s))) (F c s)
1517 (Par (N_fresh X (GV (subst_X s c (Var (F c s))))))))
1520 rewrite > (? : subst_Y (subst_X s c (Var (F c s))) (F c s)
1521 (Par (N_fresh X (GV (subst_X s c (Var (F c s)))))) =
1522 subst_X s c (Par (N_fresh X (GV (subst_X s c (Var (F c s)))))))
1523 [rewrite > (? : n = S (pred n))
1527 |(* H3 *) elim daemon]
1528 |(* H3 *) elim daemon]
1529 |rewrite < subst_X_decompose
1531 |rewrite > (L_to_closed F)
1535 |intro;reflexivity]]
1537 |rewrite < subst_X_decompose
1538 [rewrite > subst_X_fp
1539 [rewrite < (swap_left X c) in ⊢ (? ? (? ? ? (? ? % ?)) ?);
1542 |rewrite > (L_to_closed F)
1546 |intro;reflexivity]]
1550 inductive typ : Type ≝
1552 | Fun : typ → typ → typ.
1554 notation "hvbox(a break ▸ b)"
1555 left associative with precedence 50
1556 for @{ 'blacktriangleright $a $b }.
1557 interpretation "STT arrow type" 'blacktriangleright a b = (Fun a b).
1559 include "datatypes/constructors.ma".
1561 definition DOM : list (X × typ) → list X ≝ λC.map ?? (fst ??) C.
1563 inductive context : list (X × typ) → Prop ≝
1564 | ctx_nil : context []
1565 | ctx_cons : ∀x,t,C.x ∉ DOM C → context C → context (〈x,t〉::C).
1568 inductive typing (F:xheight): list (X × typ) → S_exp → typ → Prop ≝
1569 | t_axiom : ∀C,x,t.context C → 〈x,t〉 ∈ C → typing F C (Par x) t
1570 | t_App : ∀C,M,N,t,u.typing F C M (t ▸ u) → typing F C N t →
1571 typing F C (App M N) u
1572 | t_Lam : ∀C,x,M,t,u.x ∉ DOM C → typing F (〈x,t〉::C) M u →
1573 typing F C (Abs (F x M) (subst_X M x (Var (F x M)))) (t ▸ u).
1575 inductive typing2 (F:xheight): list (X × typ) → S_exp → typ → Prop ≝
1576 | t2_axiom : ∀C,x,t.context C → 〈x,t〉 ∈ C → typing2 F C (Par x) t
1577 | t2_App : ∀C,M,N,t,u.typing2 F C M (t ▸ u) → typing2 F C N t →
1578 typing2 F C (App M N) u
1579 | t2_Lam : ∀C,x1,M,t,u.
1580 (∀x2.x2 ∉ DOM C → (x2 ∈ GV M → x2 = x1) →
1581 typing2 F (〈x2,t〉::C) (subst_X M x1 (Par x2)) u) →
1582 typing2 F C (Abs (F x1 M) (subst_X M x1 (Var (F x1 M)))) (t ▸ u).
1584 notation > "C ⊢[F] M : t"
1585 non associative with precedence 30 for @{ 'typjudg F $C $M $t }.
1586 notation > "C ⊢ M : t"
1587 non associative with precedence 30 for @{ 'typjudg ? $C $M $t }.
1588 notation < "mstyle color #007f00 (hvbox(C maction (⊢) (⊢ \sub F) break M : break t))"
1589 non associative with precedence 30 for @{ 'typjudg $F $C $M $t }.
1590 interpretation "Fsub subtype judgement" 'typjudg F C M t = (typing F C M t).
1592 notation > "C ⊨[F] M : t"
1593 non associative with precedence 30 for @{ 'typjudg2 F $C $M $t }.
1594 notation > "C ⊨ M : t"
1595 non associative with precedence 30 for @{ 'typjudg2 ? $C $M $t }.
1596 notation < "mstyle color #007f00 (hvbox(C maction (⊨) (⊨ \sub F) break M : break t))"
1597 non associative with precedence 30 for @{ 'typjudg2 $F $C $M $t }.
1598 interpretation "Fsub strong subtype judgement" 'typjudg2 F C M t = (typing2 F C M t).
1600 lemma in_ctx_to_in_DOM : ∀x,t.∀C:list (X × typ).〈x,t〉 ∈ C → x ∈ DOM C.
1602 [elim (not_in_list_nil ?? H)
1603 |elim (in_list_cons_case ???? H1)
1604 [rewrite < H2;simplify;autobatch
1605 |cases a;simplify;autobatch]]
1608 lemma in_DOM_to_in_ctx : ∀x,C.x ∈ DOM C → ∃t.〈x,t〉 ∈ C.
1610 [elim (not_in_list_nil X ? H)
1611 |elim a in H1;simplify in H1;elim (in_list_cons_case ???? H1)
1612 [rewrite > H2;autobatch
1613 |cases (H H2);autobatch]]
1616 lemma incl_DOM : ∀l1,l2. l1 ⊆ l2 → DOM l1 ⊆ DOM l2.
1617 intros;unfold in H;unfold;intros;cases (in_DOM_to_in_ctx ?? H1);autobatch;
1620 lemma typing2_weakening : ∀F,C,M,t.
1621 C ⊨[F] M : t → ∀D.context D → C ⊆ D → D ⊨[F] M : t.
1622 intros 5;elim H;try autobatch size=7;
1623 apply t2_Lam;intros;apply H2;
1628 definition swap_list : ∀N:Nset.N → N → list N → list N ≝
1629 λN,a,b,l.map ?? (pi_swap ? a b) l.
1631 lemma in_list_swap : ∀N:Nset.∀x,l.x ∈ l → ∀a,b.swap N a b x ∈ swap_list N a b l.
1632 intros;elim H;simplify;autobatch;
1635 definition ctx_swap_X : X → X → list (X × typ) → list (X × typ) ≝
1636 λx1,x2,C.map ?? (λp.
1638 [pair x t ⇒ 〈pi_swap ? x1 x2 x,t〉]) C.
1640 lemma in_ctx_swap : ∀x,t,C.〈x,t〉 ∈ C → ∀a,b.〈swap ? a b x,t〉 ∈ ctx_swap_X a b C.
1641 intros;generalize in match H;elim C;
1642 [elim (not_in_list_nil ?? H1)
1643 |simplify;inversion H2;simplify;intros;destruct;simplify;autobatch]
1646 lemma ctx_swap_X_swap_list :
1647 ∀C,x1,x2.DOM (ctx_swap_X x1 x2 C) = swap_list ? x1 x2 (DOM C).
1650 |cases a;simplify;autobatch]
1653 lemma swap_list_inv : ∀N,x1,x2,l.swap_list N x1 x2 (swap_list N x1 x2 l) = l.
1654 intros;elim l;simplify;autobatch;
1657 lemma context_eqv : ∀C.context C → ∀a,b.context (ctx_swap_X a b C).
1660 |simplify;apply ctx_cons
1661 [intro;apply H1;rewrite > ctx_swap_X_swap_list in H4;
1662 rewrite < (swap_inv ? a b);
1663 rewrite < (swap_list_inv ? a b);autobatch
1667 lemma typing_swap : ∀F:xheight.∀C,M,t,x1,x2.
1668 C ⊨[F] M : t → ctx_swap_X x1 x2 C ⊨[F] (pi_swap ? x1 x2)·M : t.
1670 [simplify;apply t2_axiom
1672 |rewrite < eq_swap_pi;autobatch]
1674 |simplify;rewrite > pi_lemma1;simplify;applyS t2_Lam;
1675 intros;rewrite < (swap_inv ? x1 x2 x);
1676 change in ⊢ (? ? ? (? ? ? %) ?) with (pi_swap X x1 x2 · Par (swap X x1 x2 x));
1677 rewrite < pi_lemma1;apply H2
1678 [intro;apply H3;rewrite < (swap_inv ? x1 x2 x);
1679 rewrite > ctx_swap_X_swap_list;autobatch
1680 |intro;rewrite > H4;autobatch]]
1683 lemma typing_to_typing2 : ∀F:xheight.∀C,M,t.C ⊢[F] M : t → C ⊨[F] M : t.
1684 intros;elim H;try autobatch;
1685 apply t2_Lam;intros;
1686 rewrite > subst_X_fp
1687 [rewrite > (? : 〈x2,t1〉::l = ctx_swap_X c x2 (〈c,t1〉::l))
1689 |simplify;rewrite < eq_swap_pi;rewrite > swap_left;
1690 rewrite < (? : l = ctx_swap_X c x2 l)
1692 |generalize in match H1;generalize in match H4;elim l 0
1694 |intro;cases a;simplify;intros;
1695 rewrite < eq_swap_pi;rewrite > swap_other
1699 |*:intro;autobatch]]]]
1703 lemma typing2_to_typing : ∀F:xheight.∀C,M,t.C ⊨[F] M : t → C ⊢[F] M : t.
1704 intros;elim H;try autobatch;
1705 generalize in match (p_fresh ? (c::DOM l@GV s));
1706 generalize in match (N_fresh ? (c::DOM l@GV s));
1709 [rewrite > subst_X_fp in Hletin
1710 [lapply (t_Lam ??????? Hletin)
1711 [intro;apply f_xn;autobatch
1712 |rewrite < subst_X_fp in Hletin1
1713 [rewrite > subst_X_merge in Hletin1
1714 [rewrite < (? : F c s = F xn (subst_X s c (Par xn))) in Hletin1
1716 |rewrite > subst_X_fp
1717 [rewrite < (swap_left ? c xn) in ⊢ (? ? ? (? ? % ?));
1718 rewrite > eq_swap_pi;autobatch]]]]]]]
1719 intro;elim f_xn;autobatch;