--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "lambda.ma".
+
+(*
+ * beta reduction relation
+ * EASY TO SEE THAT BETA IS EQUIVARIANT, IMPLIES WELL-FORMEDNESS AND
+ * DOES NOT CREATE NEW FREE GLOBAL VARIABLES
+ *)
+inductive beta (F: X → S_exp → Y) : S_exp → S_exp → Prop ≝
+| b_redex : ∀y,M,N.L F (Abs y M) → L F N →
+ beta F (App (Abs y M) N) (subst_Y M y N)
+| b_app1 : ∀M1,M2,N.beta F M1 M2 → L F N → beta F (App M1 N) (App M2 N)
+| b_app2 : ∀M,N1,N2.L F M → beta F N1 N2 → beta F (App M N1) (App M N2)
+| b_xi : ∀M,N,x.beta F M N → beta F (Abs (F x M) (subst_X M x (Var (F x M))))
+ (Abs (F x N) (subst_X N x (Var (F x N)))).
+
+(* parallel reduction relation, should have the same properties *)
+inductive pr (F: X → S_exp → Y) : S_exp → S_exp → Prop ≝
+| pr_par : ∀x.pr F (Par x) (Par x)
+| pr_redex : ∀x,M1,M2,N1,N2.pr F M1 M2 → pr F N1 N2 →
+ pr F (App (Abs (F x M1) (subst_X M1 x (Var (F x M1)))) N1)
+ (subst_X M2 x N2)
+| pr_app : ∀M1,M2,N1,N2.pr F M1 M2 → pr F N1 N2 → pr F (App M1 N1) (App M2 N2)
+| pr_xi : ∀M,N,x.pr F M N → pr F (Abs (F x M) (subst_X M x (Var (F x M))))
+ (Abs (F x N) (subst_X N x (Var (F x N)))).
+
+(* complete development relation, should have the same properties *)
+inductive cd (F: X → S_exp → Y) : S_exp → S_exp → Prop ≝
+| cd_par : ∀x.cd F (Par x) (Par x)
+| cd_redex : ∀x,M1,M2,N1,N2.cd F M1 M2 → cd F N1 N2 →
+ cd F (App (Abs (F x M1) (subst_X M1 x (Var (F x M1)))) N1)
+ (subst_X M2 x N2)
+| cd_app : ∀M1,M2,N1,N2.(∀y,P.M1 ≠ Abs y P) →
+ cd F M1 M2 → cd F N1 N2 → cd F (App M1 N1) (App M2 N2)
+| cd_xi : ∀M,N,x.cd F M N → cd F (Abs (F x M) (subst_X M x (Var (F x M))))
+ (Abs (F x N) (subst_X N x (Var (F x N)))).
+
+notation < "hvbox(a break maction (>) (> \sub f) b)"
+ non associative with precedence 45
+for @{ 'gt $f $a $b }.
+notation < "hvbox(a break maction (≫) (≫\sub f) b)"
+ non associative with precedence 45
+for @{ 'ggt $f $a $b }.
+notation < "hvbox(a break maction (⋙) (⋙\sub f) b)"
+ non associative with precedence 45
+for @{ 'gggt $f $a $b }.
+
+notation > "hvbox(a break >[f] b)"
+ non associative with precedence 45
+for @{ 'gt $f $a $b }.
+notation > "hvbox(a break ≫[f] b)"
+ non associative with precedence 45
+for @{ 'ggt $f $a $b }.
+notation > "hvbox(a break ⋙[f] b)"
+ non associative with precedence 45
+for @{ 'gggt $f $a $b }.
+
+interpretation "pollack-sato beta reduction" 'gt F M N = (beta F M N).
+interpretation "pollack-sato parallel reduction" 'ggt F M N = (pr F M N).
+interpretation "pollack-sato complete development" 'gggt F M N = (cd F M N).
+
+lemma cd_exists : ∀F:xheight.∀M.L F M → ∃N.M ⋙[F] N.
+intros;elim H
+[autobatch
+|generalize in match H2;generalize in match H1;clear H1 H2;cases s;intros
+ [1,2,3:cases H2;cases H4;exists [1,3,5:apply (App x x1)]
+ apply cd_app
+ [1,4,7:intros;intro;destruct
+ |*:assumption]
+ |inversion H1;simplify;intros;destruct;clear H5 H6;
+ cases H2;clear H2;inversion H5;simplify;intros;destruct;
+ cases H4;clear H4 H6;exists
+ [2:apply cd_redex
+ [3:apply H2
+ |4:apply H7
+ |*:skip]
+ |skip]]
+|cases H2;clear H2;exists
+ [|apply cd_xi
+ [|apply H3]]]
+qed.
+
+axiom pi_swap_inv : ∀u,v,M.pi_swap ? u v · (pi_swap ? u v · M) = M.
+
+(* useless... *)
+lemma pr_swap : ∀F:xheight.∀M,N,x1,x2.
+ M ≫[F] N → pi_swap ? x1 x2 · M ≫[F] pi_swap ? x1 x2 · N.
+intros;elim H
+[simplify;autobatch
+|simplify;do 2 rewrite > pi_lemma1;simplify;
+ rewrite > (? : F c s = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s));
+ autobatch
+|simplify;autobatch
+|simplify;do 2 rewrite > pi_lemma1;simplify;
+ rewrite > (? : F c s = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s));
+ [rewrite > (? : F c s1 = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s1));
+ autobatch
+ |autobatch]]
+qed.
+
+inductive pr2 (F: X → S_exp → Y) : S_exp → S_exp → Prop ≝
+| pr2_par : ∀x.pr2 F (Par x) (Par x)
+| pr2_redex : ∀x1,M1,M2,N1,N2.
+ (∀x2.(x2 ∈ GV M1 → x2 = x1) →
+ pr2 F (subst_X M1 x1 (Par x2)) (subst_X M2 x1 (Par x2))) →
+ pr2 F N1 N2 →
+ pr2 F (App (Abs (F x1 M1) (subst_X M1 x1 (Var (F x1 M1)))) N1)
+ (subst_X M2 x1 N2)
+| pr2_app : ∀M1,M2,N1,N2.pr2 F M1 M2 → pr2 F N1 N2 → pr2 F (App M1 N1) (App M2 N2)
+| pr2_xi : ∀M,N,x1.
+ (∀x2.(x2 ∈ GV M → x2 = x1) →
+ pr2 F (subst_X M x1 (Par x2)) (subst_X N x1 (Par x2))) →
+ pr2 F (Abs (F x1 M) (subst_X M x1 (Var (F x1 M))))
+ (Abs (F x1 N) (subst_X N x1 (Var (F x1 N)))).
+
+inductive np (F: X → S_exp → Y) : S_exp → S_exp → Prop ≝
+| k1 : ∀x,M1,M2,N1,N2.np F M1 M2 → np F N1 N2 →
+ np F (App (Abs (F x M1) (subst_X M1 x (Var (F x M1)))) N1)
+ (subst_X M2 x N2).
+
+(*lemma np_strong_swap : ∀F:X→S_exp→Y.∀P:S_exp→S_exp→Prop.
+ (∀c:X.
+ ∀s:S_exp.
+ ∀s1:S_exp.
+ ∀s2:S_exp.
+ ∀s3:S_exp.
+ (∀x.(x ∈ GV s → x = c) →
+ P (subst_X s c (Par x)) (subst_X s1 c (Par x))) →
+ P s2 s3 →
+ P (App (Abs (F c s) (subst_X s c (Var (F c s)))) s2) (subst_X s1 c s3)) →
+ ∀s:S_exp.∀s1:S_exp.np F s s1→∀f:finite_perm X.P (f · s) (f · s1).
+intros 6;elim H1;simplify;
+rewrite > (?: f ·subst_X s3 c s5 = subst_X (f · s3) (f c) (f · s5))
+[rewrite > (?: f ·subst_X s2 c (Var (F c s2)) = subst_X (f · s2) (f c) (Var (F c s2)))
+ [rewrite > (? : F c s2 = F (f c) (f · s2))
+ [apply H
+ [intros;rewrite > subst_X_fp [|assumption]
+ rewrite > subst_X_fp [|elim daemon]
+ [
+ |apply H5]
+apply H;
+[intros;
+|assumption]*)
+
+lemma pr2_swap : ∀F:xheight.∀M,N,x1,x2.
+ pr2 F M N → pr2 F (pi_swap ? x1 x2 · M) (pi_swap ? x1 x2 · N).
+intros;elim H
+[simplify;autobatch
+|simplify;do 2 rewrite > pi_lemma1;simplify;
+ rewrite > (? : F c s = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s))
+ [apply pr2_redex
+ [intros;lapply (H2 (pi_swap ? x1 x2 x))
+ [rewrite > (? : Par x = pi_swap X x1 x2 · (Par (pi_swap X x1 x2 x)));
+ autobatch
+ |intro;rewrite < (swap_inv ? x1 x2 c);rewrite < eq_swap_pi;
+ apply eq_f;apply H5;
+ rewrite < (swap_inv ? x1 x2 x);autobatch]
+ |assumption]
+ |autobatch]
+|simplify;autobatch
+|simplify;do 2 rewrite > pi_lemma1;simplify;
+ rewrite > (? : F c s = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s));
+ [rewrite > (? : F c s1 = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s1));
+ [apply pr2_xi;intros;lapply (H2 (pi_swap ? x1 x2 x))
+ [rewrite > (? : Par x = pi_swap X x1 x2 · (Par (pi_swap X x1 x2 x)));
+ autobatch
+ |intro;rewrite < (swap_inv ? x1 x2 c);rewrite < eq_swap_pi;
+ apply eq_f;apply H3;
+ rewrite < (swap_inv ? x1 x2 x);autobatch]
+ |autobatch]
+ |autobatch]]
+qed.
+
+(* TODO : a couple of clear but not trivial open subproofs *)
+lemma pr_GV_incl : ∀F:xheight.∀M,N.M ≫[F] N → GV N ⊆ GV M.
+intros;elim H;simplify
+[autobatch
+|cut (GV (subst_X s1 c s3) ⊆ filter ? (GV s1) (λz.¬ (c ≟ z)) @ GV s3)
+ [unfold;intros;cases (in_list_append_to_or_in_list ???? (Hcut ? H5))
+ [apply in_list_to_in_list_append_l;
+ cases (GV_subst_X_Var s c (F c s) x);clear H7;apply H8;
+ (* reasoning from H2 and monotonicity of filter *)
+ elim daemon
+ |autobatch]
+ |(* boring *) elim daemon]
+|unfold;intros;cases (in_list_append_to_or_in_list ???? H5);autobatch
+|unfold;intros;cases (GV_subst_X_Var s c (F c s) x);
+ clear H4;apply H5;
+ cases (GV_subst_X_Var s1 c (F c s1) x);lapply (H4 H3);clear H4 H6;
+ (* Hletin and monotonicity of filter *)
+ elim daemon]
+qed.
+
+lemma pr_to_pr2 : ∀F:xheight.∀M,N.M ≫[F] N → pr2 F M N.
+intros;elim H
+[autobatch
+|apply pr2_redex
+ [intros;rewrite > subst_X_fp
+ [rewrite > subst_X_fp
+ [autobatch
+ |intro;apply H5;apply pr_GV_incl;
+ [3,4:autobatch
+ |*:skip]]
+ |assumption]
+ |assumption]
+|autobatch
+|apply pr2_xi;intros;rewrite > subst_X_fp
+ [rewrite > subst_X_fp
+ [autobatch
+ |intro;apply H3;apply pr_GV_incl
+ [3,4:autobatch
+ |*:skip]]
+ |assumption]]
+qed.
+
+lemma pr2_to_pr : ∀F:xheight.∀M,N.pr2 F M N → M ≫[F] N.
+intros;elim H
+[1,3:autobatch
+|apply pr_redex
+ [applyS (H2 c);intro;reflexivity
+ |assumption]
+|apply pr_xi;applyS (H2 c);intro;reflexivity]
+qed.
+
+(* ugly, must factorize *)
+lemma pr_subst_X : ∀F:xheight.∀M1,M2,x,N1,N2.
+ M1 ≫[F] M2 → N1 ≫[F] N2 →
+ subst_X M1 x N1 ≫[F] subst_X M2 x N2.
+intros;lapply (pr_to_pr2 ??? H) as H';clear H;
+generalize in match H1;generalize in match N2 as N2;generalize in match N1 as N1;
+clear H1 N1 N2;
+elim H'
+[simplify;apply (bool_elim ? (x ≟ c));simplify;intro;autobatch
+|generalize in match (p_fresh ? (x::GV s @GV N1));
+ generalize in match (N_fresh ??);
+ intros (c1 Hc1);
+ rewrite > (?: Abs (F c s) (subst_X s c (Var (F c s))) =
+ Abs (F c1 (pi_swap ? c c1 · s))
+ (subst_X (pi_swap ? c c1 · s) c1 (Var (F c1 (pi_swap ? c c1 · s)))))
+ [rewrite > (?: subst_X s1 c s3 = subst_X (pi_swap ? c c1 · s1) c1 s3)
+ [simplify;rewrite > subst_X_lemma
+ [rewrite > subst_X_lemma in ⊢ (???%)
+ [rewrite > (?: F c1 (pi_swap ? c c1 · s) =
+ F c1 (subst_X (pi_swap ? c c1 · s) x N1))
+ [simplify in ⊢ (? ? (? (? ? (? ? ? %)) ?) ?);apply pr_redex
+ [rewrite < subst_X_fp
+ [rewrite < subst_X_fp
+ [apply H1
+ [intro Hfalse;elim Hc1;autobatch
+ |assumption]
+ |intro Hfalse;elim Hc1;
+ apply in_list_cons;apply in_list_to_in_list_append_l;
+ lapply (H c) [|intro;reflexivity]
+ lapply (pr2_to_pr ??? Hletin);
+ do 2 rewrite > subst_X_x_x in Hletin1;
+ apply (pr_GV_incl ??? Hletin1);assumption]
+ |intro Hfalse;elim Hc1;autobatch]
+ |autobatch]
+ |apply p_eqb1;apply XHP
+ [apply p_eqb4;intro Hfalse;apply Hc1;rewrite > Hfalse;autobatch
+ |apply apart_to_apartb_true;unfold;autobatch]]
+ |*:intro Hfalse;autobatch]
+ |*:intro Hfalse;autobatch]
+ |rewrite < subst_X_fp
+ [rewrite > subst_X_merge
+ [reflexivity
+ |intro Hfalse;autobatch]
+ |intro Hfalse;elim Hc1;
+ apply in_list_cons;apply in_list_to_in_list_append_l;
+ lapply (H c) [|intro;reflexivity]
+ do 2 rewrite > subst_X_x_x in Hletin;
+ lapply (pr2_to_pr ??? Hletin);autobatch]]
+ |rewrite < (swap_left ? c c1) in ⊢ (? ? ? (? (??%?) (? ? % (? (? ? % ?)))));
+ rewrite > eq_swap_pi;rewrite < XHE;
+ change in ⊢ (???(??(???%))) with (pi_swap ? c c1 · (Var (F c s)));
+ rewrite < pi_lemma1;rewrite < subst_X_fp
+ [rewrite > (subst_X_apart ?? (Par c1))
+ [reflexivity
+ |elim daemon (* don't we have a lemma? *)]
+ |intro Hfalse;elim Hc1;
+ apply in_list_cons;apply in_list_to_in_list_append_l;(* lemma?? *) elim daemon]]
+|simplify;autobatch
+|generalize in match (p_fresh ? (x::GV s @GV N1));
+ generalize in match (N_fresh ??);
+ intros (c1 Hc1);
+ rewrite > (?: Abs (F c s) (subst_X s c (Var (F c s))) =
+ Abs (F c1 (pi_swap ? c c1 · s))
+ (subst_X (pi_swap ? c c1 · s) c1 (Var (F c1 (pi_swap ? c c1 · s)))));
+ [rewrite > (?: Abs (F c s1) (subst_X s1 c (Var (F c s1))) =
+ Abs (F c1 (pi_swap ? c c1 · s1))
+ (subst_X (pi_swap ? c c1 · s1) c1 (Var (F c1 (pi_swap ? c c1 · s1)))));
+ [simplify;rewrite > subst_X_lemma
+ [rewrite > subst_X_lemma in ⊢ (???%)
+ [simplify;rewrite > (? : F c1 (pi_swap ? c c1 · s) = F c1 (subst_X (pi_swap ? c c1 · s) x N1))
+ [rewrite > (? : F c1 (pi_swap ? c c1 · s1) = F c1 (subst_X (pi_swap ? c c1 · s1) x N2))
+ [apply pr_xi;rewrite < subst_X_fp
+ [rewrite < subst_X_fp
+ [apply H1
+ [intro Hfalse;elim Hc1;autobatch
+ |assumption]
+ |intro Hfalse; (* meglio fare qualcosa di più furbo *) elim daemon]
+ |intro;elim Hc1;autobatch]
+ |apply p_eqb1;apply XHP
+ [apply p_eqb4;intro Hfalse;autobatch
+ |apply apart_to_apartb_true;intro;autobatch]]
+ |apply p_eqb1;apply XHP
+ [apply p_eqb4;intro Hfalse;autobatch
+ |apply apart_to_apartb_true;intro;autobatch]]
+ |*:intro;apply Hc1;autobatch]
+ |*:intro;apply Hc1;autobatch]
+ |apply eq_f2
+ [autobatch
+ |rewrite < (swap_left ? c c1) in ⊢ (??? (??% (? (??%?))));
+ rewrite > eq_swap_pi;rewrite < XHE;
+ change in ⊢ (???(???%)) with (pi_swap ? c c1 · (Var (F c s1)));
+ rewrite < pi_lemma1;rewrite < subst_X_fp
+ [rewrite > (subst_X_apart ?? (Par c1))
+ [reflexivity
+ |elim daemon (* don't we have a lemma? *)]
+ |intro Hfalse;elim Hc1;
+ apply in_list_cons;apply in_list_to_in_list_append_l;(* lemma?? *) elim daemon]]]
+ |apply eq_f2
+ [autobatch
+ |rewrite < (swap_left ? c c1) in ⊢ (??? (??% (? (??%?))));
+ rewrite > eq_swap_pi;rewrite < XHE;
+ change in ⊢ (???(???%)) with (pi_swap ? c c1 · (Var (F c s)));
+ rewrite < pi_lemma1;rewrite < subst_X_fp
+ [rewrite > (subst_X_apart ?? (Par c1))
+ [reflexivity
+ |elim daemon (* don't we have a lemma? *)]
+ |intro Hfalse;elim Hc1;
+ apply in_list_cons;apply in_list_to_in_list_append_l;(* lemma?? *) elim daemon]]]]
+qed.
+
+lemma L_subst_X : ∀F:xheight.∀M,x,N.L F M → L F N → L F (subst_X M x N).
+intros;elim (L_to_LL ?? H);
+[simplify;cases (x ≟ c);simplify;autobatch
+|simplify;autobatch
+|generalize in match (p_fresh ? (x::GV s @GV N));
+ generalize in match (N_fresh ??);
+ intros (c1 Hc1);
+ rewrite > (?: Abs (F c s) (subst_X s c (Var (F c s))) =
+ Abs (F c1 (pi_swap ? c c1 · s))
+ (subst_X (pi_swap ? c c1 · s) c1 (Var (F c1 (pi_swap ? c c1 · s)))));
+ [simplify;rewrite > subst_X_lemma
+ [simplify;rewrite > (? : F c1 (pi_swap ? c c1 · s) = F c1 (subst_X (pi_swap ? c c1 · s) x N))
+ [apply LAbs;rewrite < subst_X_fp
+ [apply H3;intro Hfalse;elim Hc1;autobatch
+ |intro Hfalse;elim Hc1;autobatch]
+ |apply p_eqb1;apply XHP
+ [apply p_eqb4;intro Hfalse;autobatch
+ |apply apart_to_apartb_true;intro;autobatch]]
+ |*:intro;apply Hc1;autobatch]
+ |apply eq_f2
+ [autobatch
+ |rewrite < (swap_left ? c c1) in ⊢ (??? (??% (? (??%?))));
+ rewrite > eq_swap_pi;rewrite < XHE;
+ change in ⊢ (???(???%)) with (pi_swap ? c c1 · (Var (F c s)));
+ rewrite < pi_lemma1;rewrite < subst_X_fp
+ [rewrite > (subst_X_apart ?? (Par c1))
+ [reflexivity
+ |elim daemon (* don't we have a lemma? *)]
+ |intro Hfalse;elim Hc1;
+ apply in_list_cons;apply in_list_to_in_list_append_l;
+ (* lemma?? *) elim daemon]]]]
+qed.
+
+inductive cd2 (F: X → S_exp → Y) : S_exp → S_exp → Prop ≝
+| cd2_par : ∀x.cd2 F (Par x) (Par x)
+| cd2_redex : ∀x,M1,M2,N1,N2.
+ (∀x2.(x2 ∈ GV M1 → x2 = x) →
+ cd2 F (subst_X M1 x (Par x2)) (subst_X M2 x (Par x2))) →
+ cd2 F N1 N2 →
+ cd2 F (App (Abs (F x M1) (subst_X M1 x (Var (F x M1)))) N1)
+ (subst_X M2 x N2)
+| cd2_app : ∀M1,M2,N1,N2.(∀y,P.M1 ≠ Abs y P) →
+ cd2 F M1 M2 → cd2 F N1 N2 → cd2 F (App M1 N1) (App M2 N2)
+| cd2_xi : ∀M,N,x.(∀x2.(x2 ∈ GV M → x2 = x) →
+ cd2 F (subst_X M x (Par x2)) (subst_X N x (Par x2))) →
+ cd2 F (Abs (F x M) (subst_X M x (Var (F x M))))
+ (Abs (F x N) (subst_X N x (Var (F x N)))).
+
+lemma cd2_swap : ∀F:xheight.∀M,N,x1,x2.
+ cd2 F M N → cd2 F (pi_swap ? x1 x2 · M) (pi_swap ? x1 x2 · N).
+intros;elim H
+[simplify;autobatch
+|simplify;do 2 rewrite > pi_lemma1;simplify;
+ rewrite > (? : F c s = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s))
+ [apply cd2_redex
+ [intros;lapply (H2 (pi_swap ? x1 x2 x))
+ [rewrite > (? : Par x = pi_swap X x1 x2 · (Par (pi_swap X x1 x2 x)));
+ autobatch
+ |intro;rewrite < (swap_inv ? x1 x2 c);rewrite < eq_swap_pi;
+ apply eq_f;apply H5;
+ rewrite < (swap_inv ? x1 x2 x);autobatch]
+ |assumption]
+ |autobatch]
+|simplify;apply cd2_app;
+ [intros;generalize in match H1;cases s;simplify;intros 2;destruct;
+ elim H6;[3:reflexivity|*:skip]
+ |*:assumption]
+|simplify;do 2 rewrite > pi_lemma1;simplify;
+ rewrite > (? : F c s = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s));
+ [rewrite > (? : F c s1 = F (pi_swap ? x1 x2 c) (pi_swap ? x1 x2 · s1));
+ [apply cd2_xi;intros;lapply (H2 (pi_swap ? x1 x2 x))
+ [rewrite > (? : Par x = pi_swap X x1 x2 · (Par (pi_swap X x1 x2 x)));
+ autobatch
+ |intro;rewrite < (swap_inv ? x1 x2 c);rewrite < eq_swap_pi;
+ apply eq_f;apply H3;
+ rewrite < (swap_inv ? x1 x2 x);autobatch]
+ |autobatch]
+ |autobatch]]
+qed.
+
+lemma cd_GV_incl : ∀F:xheight.∀M,N.M ⋙[F] N → GV N ⊆ GV M.
+intros;elim H;simplify
+[autobatch
+|cut (GV (subst_X s1 c s3) ⊆ filter ? (GV s1) (λz.¬ (c ≟ z)) @ GV s3)
+ [unfold;intros;cases (in_list_append_to_or_in_list ???? (Hcut ? H5))
+ [apply in_list_to_in_list_append_l;
+ cases (GV_subst_X_Var s c (F c s) x);clear H7;apply H8;
+ (* reasoning from H2 and monotonicity of filter *)
+ elim daemon
+ |autobatch]
+ |(* boring *) elim daemon]
+|unfold;intros;cases (in_list_append_to_or_in_list ???? H6);autobatch
+|unfold;intros;cases (GV_subst_X_Var s c (F c s) x);
+ clear H4;apply H5;
+ cases (GV_subst_X_Var s1 c (F c s1) x);lapply (H4 H3);clear H4 H6;
+ (* Hletin and monotonicity of filter *)
+ elim daemon]
+qed.
+
+lemma cd_to_cd2 : ∀F:xheight.∀M,N.M ⋙[F] N → cd2 F M N.
+intros;elim H
+[autobatch
+|apply cd2_redex
+ [intros;rewrite > subst_X_fp
+ [rewrite > subst_X_fp
+ [autobatch
+ |intro;apply H5;apply cd_GV_incl;
+ [3,4:autobatch
+ |*:skip]]
+ |assumption]
+ |assumption]
+|autobatch
+|apply cd2_xi;intros;rewrite > subst_X_fp
+ [rewrite > subst_X_fp
+ [autobatch
+ |intro;apply H3;apply cd_GV_incl
+ [3,4:autobatch
+ |*:skip]]
+ |assumption]]
+qed.
+
+lemma pr_cd_triangle : ∀F:xheight.∀M,N,P.M ≫[F] N → M ⋙[F] P → N ≫[F] P.
+intros;generalize in match H;generalize in match N;clear H N;
+elim (cd_to_cd2 ??? H1)
+[inversion H;simplify;intros;destruct;autobatch
+|inversion (pr_to_pr2 ??? H5);simplify;intros;destruct;
+ [clear H7 H9;
+ lapply (H4 ? (pr2_to_pr ??? H8)) as H9;clear H4;
+ generalize in match (p_fresh ? (GV s));
+ generalize in match (N_fresh ? (GV s));intros;
+ rewrite > (? : subst_X s6 c1 s8 = subst_X (subst_X s6 c1 (Par c2)) c2 s8)
+ [rewrite > (? : subst_X s1 c s3 = subst_X (subst_X s1 c (Par c2)) c2 s3)
+ [apply pr_subst_X
+ [apply H2;
+ [intro;elim H4;assumption
+ |rewrite > (? : subst_X s c (Par c2) = subst_X s5 c1 (Par c2))
+ [apply pr2_to_pr;apply H6;intro; (* must be fresh in s5 *) elim daemon
+ |(* by Hcut2 *) elim daemon]]
+ |assumption]
+ |(* as long as it's fresh in s1 too *) elim daemon]
+ |(* as long as it's fresh in s6 too *) elim daemon]
+ |lapply (H4 ? (pr2_to_pr ??? H8));inversion H6;intros;simplify;destruct;
+ clear H11 H7 H9;
+ generalize in match (p_fresh ? (GV s));
+ generalize in match (N_fresh ? (GV s));intros;
+ rewrite > (? : subst_X s5 c1 (Var (F c1 s5)) = subst_X (subst_X s5 c1 (Par c2)) c2 (Var (F c1 s5)))
+ [rewrite > (? : F c1 s5 = F c2 (subst_X s5 c1 (Par c2)))
+ [rewrite > (? : subst_X s1 c s3 = subst_X (subst_X s1 c (Par c2)) c2 s3)
+ [apply pr_redex
+ [apply H2
+ [intro;elim H7;assumption
+ |rewrite > (?: subst_X s c (Par c2) = subst_X s4 c1 (Par c2))
+ [apply pr2_to_pr;apply H10;(* suff fresh *) elim daemon
+ |(* by Hcut1 *) elim daemon]]
+ |assumption]
+ |(* suff. fresh *) elim daemon]
+ |(* eqvariance *) elim daemon]
+ |(* eqvariance *) elim daemon]]
+|inversion H6;simplify;intros;destruct;
+ [elim H [3:reflexivity|*:skip]
+ |autobatch]
+|inversion (pr_to_pr2 ??? H3);simplify;intros;destruct;clear H5;
+ generalize in match (p_fresh ? (GV s));
+ generalize in match (N_fresh ? (GV s));intros;
+ rewrite > (?: subst_X s4 c1 (Var (F c1 s4)) = subst_X (subst_X s4 c1 (Par c2)) c2 (Var (F c1 s4)))
+ [rewrite > (?: subst_X s1 c (Var (F c s1)) = subst_X (subst_X s1 c (Par c2)) c2 (Var (F c s1)))
+ [rewrite > (?: F c1 s4 = F c2 (subst_X s4 c1 (Par c2)))
+ [rewrite > (?: F c s1 = F c2 (subst_X s1 c (Par c2)))
+ [apply pr_xi;apply H2
+ [intro;elim H5;assumption
+ |rewrite > (?: subst_X s c (Par c2) = subst_X s3 c1 (Par c2))
+ [apply pr2_to_pr;apply H4;(*suff. fresh*) elim daemon
+ |(*by Hcut1*)elim daemon]]
+ |(*perm*)elim daemon]
+ |(*perm*)elim daemon]
+ |(*suff.fresh*) elim daemon]
+ |(*suff.fresh*) elim daemon]]
+ qed.
+
+lemma diamond_pr : ∀F:xheight.∀a,b,c.a ≫[F] b → a ≫[F] c →
+ ∃d.b ≫[F] d ∧ c ≫[F] d.
+intros;
+cut (L F a)
+[cases (cd_exists ?? Hcut) (d);
+ exists[apply d]
+ split;autobatch;
+|elim H;autobatch]
+qed.
+
+inductive tc (A:Type) (R:A → A → Prop) : A → A → Prop ≝
+| tc_refl : ∀x:A.tc A R x x
+| tc_trans : ∀x,y,z.R x y → tc A R y z → tc A R x z.
+
+lemma strip_tc_pr : ∀F:xheight.∀a,b,c.pr F a b → tc ? (pr F) a c →
+ ∃d.tc ? (pr F) b d ∧ pr F c d.
+intros;generalize in match H;generalize in match b;clear H b;elim H1
+[autobatch;
+|cases (diamond_pr ???? H H4);cases H5;clear H5;
+ cases (H3 ? H6);cases H5;clear H5;exists[apply x1]
+ split;autobatch]
+qed.
+
+lemma diamond_tc_pr : ∀F:xheight.∀a,b,c.tc ? (pr F) a b → tc ? (pr F) a c →
+ ∃d.tc ? (pr F) b d ∧ tc ? (pr F) c d.
+intros 5;generalize in match c; clear c;elim H
+[autobatch;
+|cases (strip_tc_pr ???? H1 H4);cases H5;clear H5;
+ cases (H3 ? H6);cases H5;clear H5;
+ exists[apply x1]
+ split;autobatch]
+qed.
+
+lemma tc_split : ∀A,R,a,b,c.tc A R a b → tc A R b c → tc A R a c.
+intros 6;elim H;autobatch;
+qed.
+
+lemma tc_single : ∀A,R,a,b.R a b → tc A R a b.
+intros;autobatch;
+qed.
+
+lemma tcb_app1 : ∀F:xheight.∀M1,M2,N.tc ? (beta F) M1 M2 → L F N →
+ tc ? (beta F) (App M1 N) (App M2 N).
+intros;elim H;autobatch;
+qed.
+
+lemma tcb_app2 : ∀F:xheight.∀M,N1,N2.L F M → tc ? (beta F) N1 N2 →
+ tc ? (beta F) (App M N1) (App M N2).
+intros;elim H1;autobatch;
+qed.
+
+lemma tcb_xi : ∀F:xheight.∀M,N,x.
+ tc ? (beta F) M N →
+ tc ? (beta F) (Abs (F x M) (subst_X M x (Var (F x M))))
+ (Abs (F x N) (subst_X N x (Var (F x N)))).
+intros;elim H;autobatch;
+qed.
+
+lemma red_lemma :
+ ∀F:xheight.∀x,M,N.L F M →
+ subst_X M x N = subst_Y (subst_X M x (Var (F x M))) (F x M) N.
+intros;rewrite < subst_X_decompose;
+[reflexivity
+|rewrite > L_to_closed;autobatch
+|autobatch]
+qed.
+
+lemma b_redex2 :
+ ∀F:xheight.∀x,M,N.L F M → L F N →
+ beta F (App (Abs (F x M) (subst_X M x (Var (F x M)))) N) (subst_X M x N).
+intros;rewrite > (red_lemma ???? H) in ⊢ (???%);
+apply b_redex;autobatch;
+qed.
+
+lemma pr_to_L_1 : ∀F:xheight.∀a,b.a ≫[F] b → L F a.
+intros;elim H;autobatch;
+qed.
+
+lemma pr_to_L_2 : ∀F:xheight.∀a,b.a ≫[F] b → L F b.
+intros;elim H;autobatch;
+qed.
+
+lemma pr_to_tc_beta : ∀F:xheight.∀a,b.a ≫[F] b → tc ? (beta F) a b.
+intros;elim H
+[autobatch
+|apply (tc_split ?????? (?: tc ? (beta F) (App (Abs (F c s) (subst_X s c (Var (F c s)))) s3) ?));
+ [apply tcb_app2;autobatch
+ |apply (tc_split ?????? (?: tc ? (beta F) (App (Abs (F c s1) (subst_X s1 c (Var (F c s1)))) s3) ?));
+ [apply tcb_app1;autobatch
+ |apply tc_single;apply b_redex2;autobatch]]
+|apply (tc_split ????? (?: tc ?? (App s s2) (App s s3)))
+ [apply tcb_app2;autobatch
+ |apply tcb_app1;autobatch]
+|autobatch]
+qed.
+
+lemma pr_refl : ∀F:xheight.∀a.L F a → a ≫[F] a.
+intros;elim H;try autobatch;
+qed.
+
+lemma tc_pr_to_tc_beta: ∀F:xheight.∀a,b.tc ? (pr F) a b → tc ? (beta F) a b.
+intros;elim H;autobatch;
+qed.
+
+lemma beta_to_pr : ∀F:xheight.∀a,b.a >[F] b → a ≫[F] b.
+intros;elim H
+[inversion H1;intros;destruct;
+ rewrite < subst_X_decompose
+ [autobatch
+ |rewrite > (L_to_closed ?? H3);autobatch
+ |autobatch]
+|2,3:apply pr_app;autobatch
+|apply pr_xi;assumption]
+qed.
+
+lemma tc_beta_to_tc_pr: ∀F:xheight.∀a,b.tc ? (beta F) a b → tc ? (pr F) a b.
+intros;elim H;autobatch;
+qed.
+
+theorem church_rosser:
+ ∀F:xheight.∀a,b,c.tc ? (beta F) a b → tc ? (beta F) a c →
+ ∃d.tc ? (beta F) b d ∧ tc ? (beta F) c d.
+intros;lapply (tc_beta_to_tc_pr ??? H);lapply (tc_beta_to_tc_pr ??? H1);
+cases (diamond_tc_pr ???? Hletin Hletin1);cases H2;
+exists[apply x]
+split;autobatch;
+qed.
\ No newline at end of file
projects / helm.git / blobdiff