(**************************************************************** Copyright © 2009-2024 Amy Felty This file is part of "Two-Level Hybrid in Coq" This program is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version. This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with this program. If not, see . ***************************************************************) (**************************************************************** File: Hybrid.v - original: May 2009 The main library, described in: Amy Felty and Alberto Momigliano, "Hybrid: A Definitional Two Level Approach to Reasoning with Higher-Order Abstract Syntax." Journal of Automated Reasoning, 48(1):43-105, 2012. - Before 2019: updated ext_eq relation and morphisms to use current version of generalized rewriting, i.e., setoids, as described in the "Generalized Rewriting" chapter of the reference manual - Feb 2019: New definitions/lemmas, mainly about substitution - function var_notin - lemmas lbnd_level, level_greater, lbnd_proper - substitution section: bv_subst, fv_subst, subst_ty, fv_substs - for extensional equality: subst_compat, subst_ext_eq, subst as a parametric morphism - lemmas abst_app_inv, abst_app1, abst_app2, abstr_app_inv, abstr_app1, abstr_app2, abst_abs - properties of subst: subst_abst, subst_abstr, subst_abst_eq, subst_abstr_eq (subst_abstr is a key lemma) - Apr 2024: Current Coq Version: V8.18.0 ***************************************************************) Require Export Nat. Require Export BoolEq. Require Export Decidable. Require Export Lia. Require Export List. Require Export Wf_nat. Require Export Classical. Require Export ClassicalDescription. Require Export Setoid. Require Export PeanoNat. Section utils. Theorem lt_non_zero : forall i j : nat, i < j -> exists j' : nat, j = j'+1. unfold lt in |- *. intros i j; simple induction 1. - exists i; lia. - intros m H0 [j' H1]. rewrite H1. exists (j'+1); lia. Qed. End utils. (******************************************************************** Section hybrid ********************************************************************) Section hybrid. (******************************************************************** expr ********************************************************************) Set Implicit Arguments. Definition var : Set := nat. Definition bnd : Set := nat. Variable con: Set. Inductive expr : Set := CON : con -> expr | VAR : var -> expr | BND : bnd -> expr | APP : expr -> expr -> expr | ABS : expr -> expr. (******************************************************************** level and proper ********************************************************************) Inductive level : bnd -> expr -> Prop := level_CON : forall (i:bnd) (a:con), (level i (CON a)) | level_VAR : forall (i:bnd) (n:var), (level i (VAR n)) | level_BND : forall i j:bnd, (j (level i (BND j)) | level_APP : forall (i:bnd) (s t:expr), (level i s) -> (level i t) -> (level i (APP s t)) | level_ABS : forall (i:bnd) (s:expr), (level (i+1) s) -> (level i (ABS s)). Definition proper : expr -> Prop := fun e => (level 0 e). Lemma bnd_not_proper : forall i:bnd, ~(proper (BND i)). Proof. unfold proper; intros i H. inversion H. lia. Qed. Lemma proper_VAR : forall x:var, (proper (VAR x)). Proof. unfold proper; apply level_VAR. Qed. Lemma proper_APP1 : forall e1 e2:expr, (proper (APP e1 e2)) -> (proper e1). Proof. unfold proper; intros e1 e2 h; inversion h; auto. Qed. Lemma proper_APP2 : forall e1 e2:expr, (proper (APP e1 e2)) -> (proper e2). Proof. unfold proper; intros e1 e2 h; inversion h; auto. Qed. Lemma proper_APP : forall e1 e2:expr, proper e1 -> proper e2 -> (proper (APP e1 e2)). Proof. unfold proper; intros e1 e2 h1 h2. apply level_APP; auto. Qed. (******************************************************************** insts ********************************************************************) Definition elist : Set := list expr. Fixpoint insts (i:bnd)(xs:elist)(e:expr) {struct e} : expr := match e with (CON a) => (CON a) | (VAR n) => (VAR n) | (BND j) => if ((PeanoNat.Nat.leb i j) && (PeanoNat.Nat.ltb (j-i) (length xs))) then (nth (j-i) xs (BND j)) else (BND j) | (APP s t) => (APP (insts i xs s) (insts i xs t)) | (ABS s) => (ABS (insts (i+1) xs s)) end. (******************************************************************** Extensional equality of expr->expr ********************************************************************) Definition ext_eq (f g: expr -> expr) := forall x:expr, proper x -> f x = g x. Lemma ext_eq_refl : forall x : expr -> expr, ext_eq x x. Proof. unfold ext_eq; auto. Qed. Hint Resolve ext_eq_refl : Ext_Eq. Lemma ext_eq_symm : forall x y : expr -> expr, ext_eq x y -> ext_eq y x. Proof. unfold ext_eq; intros x y h1 x0 h2. specialize h1 with (1:=h2). auto. Qed. Lemma ext_eq_trans : forall x y z : expr -> expr, ext_eq x y -> ext_eq y z -> ext_eq x z. Proof. intros x y z H H0 x0 h1. generalize (H x0); generalize (H0 x0); intros H1 H2. specialize H1 with (1:=h1); specialize H2 with (1:=h1). rewrite -> H1 in H2; auto. Qed. Add Parametric Relation : (expr -> expr) ext_eq reflexivity proved by ext_eq_refl symmetry proved by ext_eq_symm transitivity proved by ext_eq_trans as ext_eq_S. Lemma ext_eq_eta : forall (e:expr -> expr), ext_eq e (fun x => e x). Proof. unfold ext_eq; auto. Qed. Lemma ext_eq_APP_elim1 : forall (f g f' g': expr -> expr), (ext_eq (fun x => (APP (f x) (g x))) (fun x => (APP (f' x) (g' x)))) -> (ext_eq f f'). Proof. unfold ext_eq; intros f g f' g' H x. generalize (H x); intro H0. intro h1; specialize H0 with (1:=h1). inversion H0; auto. Qed. Lemma ext_eq_APP_elim2 : forall (f g f' g': expr -> expr), (ext_eq (fun x => (APP (f x) (g x))) (fun x => (APP (f' x) (g' x)))) -> (ext_eq g g'). Proof. unfold ext_eq; intros f g f' g' H x. generalize (H x); intro H0. intro h1; specialize H0 with (1:=h1). inversion H0; auto. Qed. Lemma ext_eq_ABS : forall (f f': expr -> expr), (ext_eq (fun x => (ABS (f x))) (fun x => (ABS (f' x)))) -> (ext_eq f f'). Proof. unfold ext_eq; intros f f' H x. intro h1; specialize H with (1:=h1). inversion H; auto. Qed. Lemma eq_ext_eq : forall (f f':expr ->expr), f=f' -> ext_eq f f'. Proof. intros f f' H. rewrite H. apply ext_eq_refl. Qed. (******************************************************************** abst and lbnd ********************************************************************) Inductive abst_aux: bnd -> (expr->expr) -> Prop := abst_CON : forall (i:bnd) (a:con), (abst_aux i (fun x => (CON a))) | abst_id : forall (i:bnd), (abst_aux i (fun x => x)) | abst_VAR : forall (i:bnd) (n:var), (abst_aux i (fun x => (VAR n))) | abst_BND : forall (i j:bnd) (e: expr -> expr), (j (abst_aux i (fun x => (BND j))) | abst_APP : forall (i:bnd) (f g: expr -> expr), (abst_aux i f) -> (abst_aux i g) -> (abst_aux i (fun x => (APP (f x) (g x)))) | abst_ABS : forall (i:bnd) (f:expr -> expr), (abst_aux (i+1) f) -> (abst_aux i (fun x => (ABS (f x)))). Definition abst (i:bnd) (e:expr->expr) : Prop := exists e', ((ext_eq e' e) /\ (abst_aux i e')). Definition abstr := abst 0. Definition ordinary : (expr -> expr) -> Prop := fun e => (exists a, ext_eq e (fun x => (CON a))) \/ (ext_eq e (fun x => x)) \/ (exists n, ext_eq e (fun x => (VAR n))) \/ (exists j, ext_eq e (fun x => (BND j))) \/ (exists f, exists g, ext_eq e (fun x => (APP (f x) (g x)))) \/ (exists f, ext_eq e (fun x => (ABS (f x)))). Inductive lbnd_aux : bnd -> (expr -> expr) -> expr -> Prop := lbnd_CON : forall (i:bnd) (a:con), (lbnd_aux i (fun x => CON a) (CON a)) | lbnd_id : forall (i:bnd), (lbnd_aux i (fun x => x) (BND i)) | lbnd_VAR : forall (i:bnd) (n:var), (lbnd_aux i (fun x => VAR n) (VAR n)) | lbnd_BND : forall (i j:bnd), (lbnd_aux i (fun x => BND j) (BND j)) | lbnd_APP : forall (i:bnd) (f g: expr -> expr) (s t: expr), (lbnd_aux i f s) -> (lbnd_aux i g t) -> (lbnd_aux i (fun x => APP (f x) (g x)) (APP s t)) | lbnd_ABS : forall (i:bnd) (f:expr -> expr) (s:expr), (lbnd_aux (i+1) f s) -> (lbnd_aux i (fun x => ABS (f x)) (ABS s)) | lbnd_Err : forall (i:bnd) (e:expr -> expr), ~(ordinary e) -> (lbnd_aux i e (BND 0)). Definition lbnd (i:bnd) (e:expr -> expr) (t:expr) : Prop := exists e', ((ext_eq e' e) /\ (lbnd_aux i e' t)). (******************************************************************** lbnd is a total relation ********************************************************************) Fixpoint size (e:expr) : nat := match e with (CON a) => 1 | (VAR n) => 1 | (BND j) => 1 | (APP s t) => (size s)+(size t) | (ABS s) => (size s)+1 end. Lemma size_positive : forall e:expr, (size e) > 0. Proof. induction e; simpl in |- *; auto; auto with arith. Qed. Lemma size_APP1 : forall e1 e2:expr, (size e1) < (size (APP e1 e2)). Proof. simpl; intros e1 e2. generalize (size_positive e2); lia. Qed. Lemma size_APP2 : forall e1 e2:expr, (size e2) < (size (APP e1 e2)). Proof. simpl; intros e1 e2. generalize (size_positive e1); lia. Qed. Lemma size_ABS :forall e:expr, (size e) < (size (ABS e)). simpl; intro e; lia. Qed. Definition rank : (expr -> expr) -> nat := fun f => (size (f (VAR 0))). Lemma rank_APP1 : forall f g e : expr -> expr, (ext_eq e (fun x => (APP (f x) (g x)))) -> (rank f) < (rank e). Proof. unfold rank; unfold ext_eq; simpl; intros f g e H. rewrite (H (VAR 0) (proper_VAR 0)). generalize (size_positive (g (VAR 0))); intro H0. assert (0 < size (g (VAR 0))). - auto with arith. - apply (Nat.add_lt_mono_l 0 (size (g (VAR 0))) (size (f (VAR 0)))) in H1. rewrite Nat.add_0_r in H1. assumption. Qed. Lemma rank_APP2 : forall f g e : expr -> expr, (ext_eq e (fun x => (APP (f x) (g x)))) -> (rank g) < (rank e). Proof. unfold rank; unfold ext_eq; simpl; intros f g e H'. rewrite (H' (VAR 0) (proper_VAR 0)). generalize (size_positive (f (VAR 0))); intro H. assert (0 < size (f (VAR 0))). - auto with arith. - apply (Nat.add_lt_mono_r 0 (size (f (VAR 0))) (size (g (VAR 0)))) in H0. assumption. Qed. Lemma rank_ABS : forall e' e: expr -> expr, (ext_eq e (fun x => (ABS (e' x)))) -> (rank e') < (rank e). Proof. unfold rank; unfold ext_eq; simpl; intros e' e H'. rewrite (H' (VAR 0) (proper_VAR 0)). generalize (size_positive (e' (VAR 0))); intro H. assert (0 < 1). - auto with arith. - apply (Nat.add_lt_mono_l 0 1 (size (e' (VAR 0)))) in H0. rewrite Nat.add_0_r in H0. assumption. Qed. Lemma lbnd_total : forall (i:bnd) (e:expr -> expr), exists s : expr, (lbnd i e s). Proof. intros i e. assert (exists n:nat, n=(rank e)). { exists (rank e); auto. } elim H; clear H. intro x; generalize i e; clear i e. generalize (lt_wf_ind x (fun x => (forall (i : bnd) (e : expr -> expr), x = rank e -> exists s : expr, lbnd i e s))). intros H. apply H; auto. clear H. intros n H i e H0. subst. unfold rank,lbnd in H. generalize (classic (ordinary e)). intros [H1 | H1]. - generalize H1; clear H1. unfold ordinary,lbnd. intros [[a H0] | [H0 | [[n H0] | [[j H0] | [[f [g H0]] | [f H0]]]]]]. + exists (CON a); exists (fun x:expr => (CON a)); split. * apply ext_eq_symm; auto. * apply lbnd_CON. + exists (BND i); exists (fun x:expr => x); split; try (apply ext_eq_symm); auto. apply lbnd_id; apply ext_eq_refl. + exists (VAR n); exists (fun x:expr => VAR n); split; try (apply ext_eq_symm); auto. apply lbnd_VAR; apply ext_eq_refl. + exists (BND j); exists (fun x:expr => BND j); split; try (apply ext_eq_symm); auto. apply lbnd_BND; apply ext_eq_refl. + assert (rank f < rank e). apply rank_APP1 with g; auto. assert (rank g < rank e). * apply rank_APP2 with f; auto. * generalize (H (rank f) H1 i f (refl_equal (rank f))). intros [s [e' [H3 H4]]]. generalize (H (rank g) H2 i g (refl_equal (rank g))). intros [s' [e'' [H5 H6]]]. exists (APP s s'); exists (fun x : expr => APP (e' x) (e'' x)); split; try (apply ext_eq_symm); auto. -- unfold ext_eq in H0; unfold ext_eq in H3; unfold ext_eq in H5; unfold ext_eq; intros x0 h1. specialize H0 with (1:=h1); specialize H3 with (1:=h1); specialize H5 with (1:=h1). rewrite -> H0; rewrite -> H3; rewrite -> H5; auto. -- apply lbnd_APP; auto. + assert (rank f < rank e). apply rank_ABS; auto. generalize (H (rank f) H1 (i+1) f (refl_equal (rank f))). intros [s [e' [H2 H3]]]. exists (ABS s); exists (fun x : expr => ABS (e' x)); split; try (apply ext_eq_symm); auto. * unfold ext_eq in H0; unfold ext_eq in H2; unfold ext_eq; intros x0 h1. specialize H0 with (1:=h1); specialize H2 with (1:=h1). rewrite -> H0; rewrite -> H2; auto. * apply lbnd_ABS; auto. - unfold lbnd. exists (BND 0); exists e; split; [apply ext_eq_refl | apply lbnd_Err]; auto. Qed. (******************************************************************** inversion lemmas for lbnd_aux ********************************************************************) Lemma lbnd_CON_inv : forall (i:bnd) (a:con) (t:expr) (e:expr -> expr), (ext_eq e (fun x => CON a)) -> (lbnd_aux i e t) -> t=(CON a). Proof. intros i a t e H; unfold ext_eq in H; destruct 1. - apply (H (VAR 0)); apply proper_VAR; auto. - generalize (H (VAR 0) (proper_VAR 0)); discriminate 1. - generalize (H (VAR 0) (proper_VAR 0)); discriminate 1. - generalize (H (VAR 0) (proper_VAR 0)); discriminate 1. - generalize (H (VAR 0) (proper_VAR 0)); discriminate 1. - generalize (H (VAR 0) (proper_VAR 0)); discriminate 1. - elim H0; unfold ordinary,ext_eq. left; exists a; auto. Qed. Lemma lbnd_id_inv : forall (i:bnd) (t:expr) (e:expr -> expr), (ext_eq e (fun x => x)) -> (lbnd_aux i e t) -> t=(BND i). Proof. intros i t e H; unfold ext_eq in H; destruct 1; auto; try (specialize H with (1:=(proper_VAR 0)); discriminate H). - assert (proper (APP (VAR 0) (VAR 0))). { apply proper_APP; apply proper_VAR; auto. } specialize H with (1:=H0); discriminate H. - elim H0; unfold ordinary, ext_eq. right; left; auto. Qed. Lemma lbnd_VAR_inv : forall (i:bnd) (n:var) (t:expr) (e:expr -> expr), (ext_eq e (fun x => VAR n)) -> (lbnd_aux i e t) -> t=(VAR n). Proof. intros i n t e H; unfold ext_eq in H; destruct 1; auto; try (specialize H with (1:=(proper_VAR 0)); discriminate H). - assert (proper (APP (VAR 0) (VAR 0))). { apply proper_APP; apply proper_VAR; auto. } specialize H with (1:=H0); discriminate H. - specialize H with (1:=(proper_VAR n)); auto. - elim H0; unfold ordinary, ext_eq. right; right; left; exists n; auto. Qed. Lemma lbnd_BND_inv : forall (i j:bnd) (t:expr) (e:expr -> expr), (ext_eq e (fun x => BND j)) -> (lbnd_aux i e t) -> t=(BND j). Proof. intros i j t e H; unfold ext_eq in H; destruct 1; auto; try (specialize H with (1:=(proper_VAR 0)); discriminate H). - specialize H with (1:=(proper_VAR 0)); auto. - elim H0; unfold ordinary,ext_eq. right; right; right; left; exists j; auto. Qed. Lemma lbnd_APP_inv : forall (i:bnd) (t: expr) (e f g: expr -> expr), (ext_eq e (fun x => APP (f x) (g x))) -> (lbnd i e t) -> (exists s':expr, exists t':expr, (lbnd i f s') /\ (lbnd i g t') /\ t=(APP s' t')). Proof. unfold lbnd. intros i t e f g H. setoid_rewrite -> H; clear H e. intros [H]. destruct H0. destruct H1. - generalize (H0 (VAR 0) (proper_VAR 0)); discriminate 1. - generalize (H0 (VAR 0) (proper_VAR 0)); discriminate 1. - generalize (H0 (VAR 0) (proper_VAR 0)); discriminate 1. - generalize (H0 (VAR 0) (proper_VAR 0)); discriminate 1. - exists s; exists t; repeat split; auto. + exists f0; split; auto; apply ext_eq_APP_elim1 with g0 g; auto. + exists g0; split; auto; apply ext_eq_APP_elim2 with f0 f; auto. - generalize (H0 (VAR 0) (proper_VAR 0)); discriminate 1. - elim H; unfold ordinary. right; right; right; right; left; exists f; exists g; auto. Qed. Lemma lbnd_ABS_inv : forall (i:bnd) (t: expr) (e f: expr -> expr), (ext_eq e (fun x => ABS (f x))) -> (lbnd i e t) -> (exists s:expr, (lbnd (i+1) f s) /\ t=(ABS s)). Proof. unfold lbnd. intros i t e f H. setoid_rewrite -> H ; clear H e. intros [H]. destruct H0. destruct H1; try (unfold ext_eq in H0; specialize H0 with (1:=(proper_VAR 0)); discriminate H0); auto. - exists s; split; auto. exists f0; split; auto; apply ext_eq_ABS; auto. - elim H; unfold ordinary. right; right; right; right; right; exists f; auto. Qed. Lemma lbnd_Err_inv : forall (i:bnd) (t:expr) (e:expr -> expr), ~(ordinary e) -> (lbnd_aux i e t) -> t=(BND 0). Proof. intros i t e H; destruct 1; auto; elim H; unfold ordinary. - left; exists a; apply ext_eq_refl. - right; left; apply ext_eq_refl. - right; right; left; exists n; apply ext_eq_refl. - right; right; right; left; exists j; apply ext_eq_refl. - right; right; right; right; left; exists f; exists g; apply ext_eq_refl. - right; right; right; right; right; exists f; apply ext_eq_refl. Qed. (******************************************************************** lemmas about lbnd and level ********************************************************************) Lemma lbnd_level : forall (e:expr) (i:bnd), level i e -> lbnd_aux i (fun _ => e) e. Proof. intros e. induction e; try (intros i H; constructor). - apply IHe1. inversion H; auto. - apply IHe2. inversion H; auto. - apply IHe. inversion H; auto. Qed. Lemma level_greater : forall (e:expr) (j i:bnd), level i e -> j >= i -> level j e. Proof. induction e. - constructor. - constructor. - intros j i H H0. inversion H; subst. constructor. lia. - intros j i H H0. inversion H; subst; constructor. + apply IHe1 with i; auto. + apply IHe2 with i; auto. - intros j i H H0. inversion H; subst; constructor. apply IHe with (i+1); auto; lia. Qed. Lemma level_succ : forall (i:bnd) (e:expr), (level i e)->(level (i+1) e). Proof. intros i e H. apply level_greater with i; auto; lia. Qed. Lemma lbnd_proper : forall (i:bnd) (e:expr) , proper e -> lbnd_aux i (fun _ => e) e. Proof. unfold proper; intros i e H. apply lbnd_level; auto. destruct i; auto. apply level_greater with 0; auto; lia. Qed. (******************************************************************** variables and substitution ********************************************************************) Fixpoint subterm (e M:expr) : Prop := proper e /\ (e = M \/ match M with | (CON a) => False | (VAR n) => False | (BND j) => False | (APP s t) => subterm e s \/ subterm e t | (ABS s) => subterm e s end). Fixpoint bv_occurs (i:bnd) (e:expr) : Prop := match e with | (CON a) => False | (VAR n) => False | (BND j) => i = j | (APP s t) => bv_occurs i s \/ bv_occurs i t | (ABS s) => bv_occurs (i+1) s end. Fixpoint bv_subst (i:bnd) (M e:expr) : expr := match e with | (CON a) => (CON a) | (VAR n) => (VAR n) | (BND j) => if (PeanoNat.Nat.eqb i j) then M else (BND j) | (APP s t) => (APP (bv_subst i M s) (bv_subst i M t)) | (ABS s) => (ABS (bv_subst (i+1) M s)) end. Fixpoint bv_substs (i:bnd) (M:expr) (l:list expr) : list expr := match l with | nil => nil | e::l' => bv_subst i M e::bv_substs i M l' end. Fixpoint fv_subst (m:var) (M e:expr) : expr := match e with | (CON a) => (CON a) | (VAR n) => if (PeanoNat.Nat.eqb m n) then M else (VAR n) | (BND j) => (BND j) | (APP s t) => (APP (fv_subst m M s) (fv_subst m M t)) | (ABS s) => (ABS (fv_subst m M s)) end. Definition subst_ty := list (var * expr) : Set. Fixpoint fv_substs (s:subst_ty) (e:expr) := match s with | nil => e | ((n,M)::tl) => fv_subst n M (fv_substs tl e) end. Fixpoint fv_substs_cxt (s:subst_ty) (l:list expr) := match l with | nil => nil | (a::l') => (fv_substs s a::fv_substs_cxt s l') end. (* A new free variable. *) Fixpoint newvar (e:expr): var := match e with CON c => 0 | VAR v => (S v) | BND i => 0 | APP e1 e2 => max (newvar e1) (newvar e2) | ABS e' => newvar e' end. Fixpoint var_notin (n:var) (e:expr) : Prop := match e with | CON c => True | VAR v => v <> n | BND i => True | APP e1 e2 => var_notin n e1 /\ var_notin n e2 | ABS e' => var_notin n e' end. Fixpoint nvC (l:list expr) {struct l} : var := match l with nil => 0 | (a::l') => max (newvar a) (nvC l') end. Fixpoint nvS (s:subst_ty) : (var) := match s with | nil => 0 | (n,e)::tl => max (max (S n) (newvar e)) (nvS tl) end. Fixpoint fv_subst_cxt (m:var) (e:expr) (l:list expr) : list expr := match l with | nil => nil | (a::tl) => (fv_subst m e a::fv_subst_cxt m e tl) end. (******************************************************************** extensional equality and morphisms ********************************************************************) Lemma abst_compat : forall (i:bnd) (e e':expr -> expr), (ext_eq e e') -> (abst i e) <-> (abst i e'). Proof. unfold abst. intros i e e' H. split. - intros [e'' [H0 H1]]. exists e''; split; auto. rewrite -> H0; auto with Ext_Eq. - intros [e'' [H0 H1]]. exists e''; split; auto. rewrite -> H; auto with Ext_Eq. Qed. Lemma abst_ext_eq : forall (i:bnd) (e e':expr -> expr), (ext_eq e e') -> (abst i e) -> (abst i e'). Proof. apply abst_compat; auto. Qed. Add Parametric Morphism : abst with signature eq ==> ext_eq ==> iff as abst_ext_eq'. Proof. apply abst_compat; auto. Qed. Lemma abstr_compat : forall (e e':expr -> expr), (ext_eq e e') -> (abstr e) <-> (abstr e'). Proof. unfold abstr. intros e e' H; split; intro H0. - apply abst_ext_eq with e; auto. - apply abst_ext_eq with e'; auto. rewrite -> H; auto with Ext_Eq. Qed. Lemma abstr_ext_eq : forall (e e':expr -> expr), (ext_eq e e') -> (abstr e) -> (abstr e'). Proof. apply abstr_compat; auto. Qed. Add Parametric Morphism : abstr with signature ext_eq ==> iff as abstr_ext_eq'. Proof. apply abstr_compat; auto. Qed. Lemma ordinary_compat : forall (e e' : expr -> expr), (ext_eq e e') -> (ordinary e) <-> (ordinary e'). Proof. unfold ordinary. intros e e' H; split; intros [[a H0] | [H0 | [[n H0] | [[j H0] | [[f [g H0]] | [f H0]]]]]]. - left. exists a; rewrite <- H; auto. - right; left. rewrite <- H; auto. - right; right; left. exists n; rewrite <- H; auto. - right; right; right; left. exists j; rewrite <- H; auto. - right; right; right; right; left. exists f; exists g; rewrite <- H; auto. - right; right; right; right; right. exists f; rewrite <- H; auto. - left. exists a; rewrite -> H; auto. - right; left. rewrite -> H; auto. - right; right; left. exists n; rewrite -> H; auto. - right; right; right; left. exists j; rewrite -> H; auto. - right; right; right; right; left. exists f; exists g; rewrite -> H; auto. - right; right; right; right; right. exists f; rewrite -> H; auto. Qed. Lemma ordinary_ext_eq : forall (e e' : expr -> expr), (ext_eq e e') -> (ordinary e) -> (ordinary e'). Proof. apply ordinary_compat; auto. Qed. Add Parametric Morphism : ordinary with signature ext_eq ==> iff as ordinary_ext_eq'. Proof. apply ordinary_compat; auto. Qed. Lemma lbnd_compat : forall (i:bnd) (e e' : expr -> expr) (t:expr), (ext_eq e e') -> (lbnd i e t) <-> (lbnd i e' t). Proof. unfold lbnd. intros i e e' t H; split; intros [e'' [H0 H1]]. - exists e''; split; auto with Ext_Eq. rewrite -> H0; auto. - exists e''; split; auto with Ext_Eq. rewrite -> H; auto with Ext_Eq. Qed. Lemma lbnd_ext_eq : forall (i:bnd) (e e' : expr -> expr) (t:expr), (ext_eq e e') -> (lbnd i e t) -> (lbnd i e' t). Proof. apply lbnd_compat. Qed. Add Parametric Morphism : lbnd with signature eq ==> ext_eq ==> eq ==> iff as lbnd_ext_eq'. Proof. intros; apply lbnd_compat; auto. Qed. (******************************************************************** properties of ordinary, abst, and lbnd ********************************************************************) Theorem abstraction_induct : forall (P:(expr -> expr) -> Prop) (e:expr -> expr), (forall (a:con) (e':expr -> expr), ext_eq e' (fun x:expr => CON a) -> P e') -> (forall (n:var) (e':expr -> expr), ext_eq e' (fun x:expr => VAR n) -> P e') -> (forall (e':expr -> expr), ext_eq e' (fun x:expr => x) -> P e') -> (forall (j:bnd) (e':expr -> expr), ext_eq e' (fun x:expr => BND j) -> P e') -> (forall e' f g:expr -> expr, ext_eq e' (fun x:expr => (APP (f x) (g x))) -> P f -> P g -> P e') -> (forall e' f:expr -> expr, ext_eq e' (fun x:expr => (ABS (f x))) -> P f -> P e') -> (forall e':expr -> expr, ~(ordinary e') -> P e') -> P e. Proof. intros P e h1 h2 h3 h4 h5 h6 ho. assert (ha1 : (exists i:nat, i=(rank e))). { exists (rank e); auto. } elim ha1; clear ha1; intros i h7. generalize (lt_wf_ind i (fun j:nat => (forall e: expr -> expr, j = rank e -> P e))). intro h8; apply h8; clear h8; auto. clear h7 i e. intros n hInd e h7. generalize (classic (ordinary e)). intros [h8 | h8]. - generalize h8; clear h8. unfold ordinary. intros [[a h8] | [h8 | [[n' h8] | [[j h8] | [[f [g h8]] | [f h8]]]]]]. + apply h1 with a; auto. + apply h3; auto. + apply h2 with n'; auto. + apply h4 with j; auto. + generalize (rank_APP1 f g h8); generalize (rank_APP2 f g h8); intros h9 h10. assert (ha1 : (rank f = rank f)); assert (ha2 : (rank g = rank g)); auto. { subst. generalize (hInd (rank f) h10 f ha1); intro h11. generalize (hInd (rank g) h9 g ha2); intro h12. apply h5 with f g; auto. } + subst. generalize (rank_ABS f h8); intro h9. assert (ha1 : (rank f = rank f)); auto. { generalize (hInd (rank f) h9 f ha1); intro h10. apply h6 with f; auto. } - apply ho; auto. Qed. Lemma level_abst_aux : forall (i:bnd) (e:expr), level i e -> abst_aux i (fun x => e). intros i e; induction 1. - apply abst_CON; auto. - apply abst_VAR; auto. - apply abst_BND; auto. - generalize (abst_APP IHlevel1 IHlevel2); auto. - generalize (abst_ABS i IHlevel); auto. Qed. Lemma proper_abstr : forall e:expr, proper e -> abstr (fun x => e). unfold proper,abstr,abst; intros e H. exists (fun x:expr => e); split; auto with Ext_Eq. apply level_abst_aux; auto. Qed. Lemma proper_abst_aux : forall e:expr, proper e -> abst_aux 0 (fun x => e). Proof. unfold proper; intros e H. apply level_abst_aux; auto. Qed. Lemma level_lbnd_aux : forall (i:bnd) (E1:expr), level (i+1) E1 -> exists E2:expr->expr, (lbnd_aux i E2 E1). Proof. intros i E1 H. assert (exists j:bnd, j=i+1). { exists (i+1); auto. } elim H0; clear H0; intros j H0. rewrite <- H0 in H. generalize H i H0; clear H i H0. induction 1. - intros; exists (fun x:expr => (CON a)); apply lbnd_CON. - intros; exists (fun x:expr => (VAR n)); apply lbnd_VAR. - intros; exists (fun x:expr => (BND j)); apply lbnd_BND. - intros i0 H1. elim (IHlevel1 i0 H1); intros E2 H1'. elim (IHlevel2 i0 H1); intros E2' H2. exists (fun x:expr => (APP (E2 x) (E2' x))). apply lbnd_APP; auto. - intros i0 H0. assert (i+1=i+1). { auto. } elim (IHlevel i H1); intros E2 H2. subst. exists (fun x : expr => ABS (E2 x)). apply lbnd_ABS; auto. Qed. Lemma same_level_lbnd_aux : forall (i:bnd) (E1:expr), level i E1 -> exists E2:expr->expr, (lbnd_aux i E2 E1). Proof. intros i E1; induction 1. - exists (fun x:expr => (CON a)). apply lbnd_CON. - exists (fun x:expr => (VAR n)). apply lbnd_VAR. - exists (fun x:expr => (BND j)). apply lbnd_BND. - elim IHlevel1; intros E2 H1. elim IHlevel2; intros E2' H2. exists (fun x:expr => (APP (E2 x) (E2' x))). apply lbnd_APP; auto. - elim IHlevel; intros E2 H0. exists (fun x : expr => ABS (E2 x)). apply lbnd_ABS; auto. Qed. Lemma abst_aux_ordinary : forall (i:bnd) (e e':expr -> expr), abst_aux i e -> ext_eq e' e -> ordinary e'. Proof. intros i e e'; induction 1. - intro H; unfold ordinary; left. exists a; auto. - intro H; unfold ordinary; right; left; auto. - intro H; unfold ordinary; right; right; left. exists n; auto. - intro H0; unfold ordinary; right; right; right; left. exists j; auto. - intro H1; unfold ordinary; right; right; right; right; left. exists f; exists g; auto. - intro H0; unfold ordinary; right; right; right; right; right. exists f; auto. Qed. Lemma abst_ordinary_ext_eq : forall (i:bnd) (e e':expr -> expr), abst i e -> ext_eq e e' -> ordinary e. Proof. unfold abst. intros i e e' [e'' [H H0]] H1. apply abst_aux_ordinary with i e'';auto. apply ext_eq_symm; auto. Qed. Lemma abst_ordinary : forall (i:bnd) (e:expr -> expr), abst i e -> ordinary e. Proof. intros i e H. apply abst_ordinary_ext_eq with i e; auto. apply ext_eq_refl. Qed. Lemma abstr_ordinary_ext_eq : forall (e e':expr -> expr), abstr e -> ext_eq e e' -> ordinary e. Proof. unfold abstr. apply abst_ordinary_ext_eq. Qed. Lemma abstr_ordinary : forall (e:expr -> expr), abstr e -> ordinary e. Proof. intros e H. apply abstr_ordinary_ext_eq with e; auto. apply ext_eq_refl. Qed. Lemma abst_aux_lbnd_one_to_one : forall (i:bnd) (e: expr -> expr), abst_aux i e -> forall (f:expr -> expr), abst_aux i f -> forall (t:expr), lbnd i e t -> lbnd i f t -> ext_eq e f. Proof. intros i e; induction 1. (* CON case *) - intros f H t [e' [H1 H2]] [f' [H3 H4]]. generalize (lbnd_CON_inv H1 H2); intro H5; subst. inversion H4; subst; auto. (* id case *) - intro f; induction 1; auto with Ext_Eq. + intros t [e' [H1 H2]] [f' [H3 H4]]. generalize (lbnd_id_inv H1 H2); intro H5; subst. generalize (lbnd_CON_inv H3 H4); intro H5; subst. discriminate H5. + intros t [e' [H1 H2]] [f' [H3 H4]]. generalize (lbnd_id_inv H1 H2); intro H5; subst. generalize (lbnd_VAR_inv H3 H4); intro H5; subst. discriminate H5. + intros t [e' [H1 H2]] [f' [H3 H4]]. generalize (lbnd_id_inv H1 H2); intro H5; subst. generalize (lbnd_BND_inv H3 H4); intro H5; subst. inversion H5; subst. absurd (j APP (f x) (g x))); intro H5. generalize (lbnd_APP_inv f g H5 H1). intros [s' [t' [H6 [H7 H8]]]]. subst. discriminate H8. + intros t H1 [e' [H2 H3]]. generalize (lbnd_id_inv H2 H3); intro H4. generalize (ext_eq_refl (fun x : expr => APP (f x) (g x))); intro H5. generalize (lbnd_APP_inv f g H5 H1). intros [s' [t' [H6 [H7 H8]]]]. subst. discriminate H8. + intros t H1 [e' [H2 H3]]. generalize (lbnd_VAR_inv H2 H3); intro H4. generalize (ext_eq_refl (fun x : expr => APP (f x) (g x))); intro H5. generalize (lbnd_APP_inv f g H5 H1). intros [s' [t' [H6 [H7 H8]]]]. subst. discriminate H8. + intros t H1' [e' [H2 H3]]. generalize (lbnd_BND_inv H2 H3); intro H4. generalize (ext_eq_refl (fun x : expr => APP (f x) (g x))); intro H5. generalize (lbnd_APP_inv f g H5 H1'). intros [s' [t' [H6 [H7 H8]]]]. subst. discriminate H8. + clear IHabst_aux3 IHabst_aux4. intros t H1 H2. generalize (ext_eq_refl (fun x : expr => APP (f x) (g x))); intro H3. generalize (ext_eq_refl (fun x : expr => APP (f0 x) (g0 x))); intro H4. generalize (lbnd_APP_inv f g H3 H1). generalize (lbnd_APP_inv f0 g0 H4 H2). intros [s' [t' [H5 [H6 H7]]]] [s'' [t'' [H8 [H9 H10]]]]. subst. inversion H10; subst. specialize IHabst_aux1 with (1:=H1_) (2:=H8) (3:=H5). specialize IHabst_aux2 with (1:=H1_0) (2:=H9) (3:=H6). unfold ext_eq in IHabst_aux1; unfold ext_eq in IHabst_aux2; unfold ext_eq. intros x h1. rewrite -> (IHabst_aux1 x h1); rewrite -> (IHabst_aux2 x h1); auto. + intros t H2 H3. generalize (ext_eq_refl (fun x : expr => APP (f x) (g x))); intro H4. generalize (ext_eq_refl (fun x : expr => ABS (f0 x))); intro H5. generalize (lbnd_APP_inv f g H4 H2). generalize (lbnd_ABS_inv f0 H5 H3). intros [s [H6 H7]] [s' [t' [H8 [H9 H10]]]]. subst. discriminate H10. (* ABS case *) - intro f0; induction 1; auto with Ext_Eq. + intros t H1 [e' [H2 H3]]. generalize (lbnd_CON_inv H2 H3); intro H4. generalize (ext_eq_refl (fun x : expr => ABS (f x))); intro H5. generalize (lbnd_ABS_inv f H5 H1). intros [s [H6 H7]]. subst. discriminate H7. + intros t H1 [e' [H2 H3]]. generalize (lbnd_id_inv H2 H3); intro H4. generalize (ext_eq_refl (fun x : expr => ABS (f x))); intro H5. generalize (lbnd_ABS_inv f H5 H1). intros [s [H6 H7]]. subst. discriminate H7. + intros t H1 [e' [H2 H3]]. generalize (lbnd_VAR_inv H2 H3); intro H4. generalize (ext_eq_refl (fun x : expr => ABS (f x))); intro H5. generalize (lbnd_ABS_inv f H5 H1). intros [s [H6 H7]]. subst. discriminate H7. + intros t H1 [e' [H2 H3]]. generalize (lbnd_BND_inv H2 H3); intro H4. generalize (ext_eq_refl (fun x : expr => ABS (f x))); intro H5. generalize (lbnd_ABS_inv f H5 H1). intros [s [H6 H7]]. subst. discriminate H7. + intros t H2 H3. generalize (ext_eq_refl (fun x : expr => ABS (f x))); intro H4. generalize (ext_eq_refl (fun x : expr => APP (f0 x) (g x))); intro H5. generalize (lbnd_ABS_inv f H4 H2). generalize (lbnd_APP_inv f0 g H5 H3). intros [s' [t' [H8 [H9 H10]]]] [s [H6 H7]]. subst. discriminate H7. + clear IHabst_aux0. intros t H1 H2. generalize (ext_eq_refl (fun x : expr => ABS (f x))); intro H3. generalize (ext_eq_refl (fun x : expr => ABS (f0 x))); intro H4. generalize (lbnd_ABS_inv f H3 H1). generalize (lbnd_ABS_inv f0 H4 H2). intros [s' [H5 H6]] [s''[H7 H8]]. subst. inversion H8; subst. specialize IHabst_aux with (1:=H0) (2:=H7) (3:=H5). unfold ext_eq. intros x h1. rewrite -> (IHabst_aux x h1); auto. Qed. Lemma abst_lbnd_one_to_one : forall (i:bnd) (e: expr -> expr), abst i e -> forall (f:expr -> expr), abst i f -> forall (t:expr), lbnd i e t -> lbnd i f t -> ext_eq e f. Proof. unfold abst; intros i e [e' [H H0]] f [f' [H1 H2]] t H3 H4. generalize (abst_aux_lbnd_one_to_one H0 H2); intro H5. setoid_rewrite <- H; setoid_rewrite <- H1. apply H5 with t; auto. - setoid_rewrite -> H; auto with Ext_Eq. - setoid_rewrite -> H1; auto with Ext_Eq. Qed. Lemma abst_eta : forall (i:bnd) (e:expr -> expr), (abst i e) -> (abst i (fun x:expr => e x)). Proof. unfold abst. intros i e [e' [H H0]]. exists e'; split; auto. Qed. Lemma abstr_eta : forall (e:expr -> expr), (abstr e) -> (abstr (fun x:expr => e x)). Proof. unfold abstr; apply abst_eta. Qed. Lemma abst_app_inv : forall (i:bnd) (e1 e2:expr -> expr), abst i (fun x => APP (e1 x) (e2 x)) -> abst i e1 /\ abst i e2. Proof. unfold abst. intros i e1 e2 [e' [H H0]]. inversion H0; subst; auto; try (unfold ext_eq in H; generalize (H (VAR 0) (proper_VAR 0)); intro h; inversion h). split. - exists f; split; auto. unfold ext_eq; intros x H3. specialize H with (1:=H3). inversion H; auto. - exists g; split; auto. unfold ext_eq; intros x H3. specialize H with (1:=H3). inversion H; auto. Qed. Lemma abst_app1 : forall (i:bnd) (e1 e2:expr -> expr), abst i (fun x => APP (e1 x) (e2 x)) -> abst i e1. Proof. intros i e1 e2 H. apply abst_app_inv in H; tauto. Qed. Lemma abst_app2 : forall (i:bnd) (e1 e2:expr -> expr), abst i (fun x => APP (e1 x) (e2 x)) -> abst i e2. Proof. intros i e1 e2 H. apply abst_app_inv in H; tauto. Qed. Lemma abstr_app_inv : forall (e1 e2:expr -> expr), abstr (fun x => APP (e1 x) (e2 x)) -> abstr e1 /\ abstr e2. Proof. unfold abstr; apply abst_app_inv. Qed. Lemma abstr_app1 : forall (e1 e2:expr -> expr), abstr (fun x => APP (e1 x) (e2 x)) -> abstr e1. Proof. unfold abstr; apply abst_app1. Qed. Lemma abstr_app2 : forall (e1 e2:expr -> expr), abstr (fun x => APP (e1 x) (e2 x)) -> abstr e2. Proof. unfold abstr; apply abst_app2. Qed. Lemma abst_abs : forall (i:bnd) (e:expr -> expr), abst i (fun x => ABS (e x)) -> abst (i+1) e. Proof. unfold abst. intros i e [e' [H H0]]. inversion H0; subst; auto; try (unfold ext_eq in H; generalize (H (VAR 0) (proper_VAR 0)); intro h; inversion h). exists f; split; auto. unfold ext_eq; intros x H2. specialize H with (1:=H2). inversion H; auto. Qed. Lemma abst_lbnd_level : forall (i:bnd) (E:expr -> expr) (e:expr), abst i E -> lbnd i E e -> level (i+1) e. Proof. intros i E e [E' [H H0]] H1. generalize dependent E; generalize dependent e. induction H0; auto. - intros e E H [e' [H0 H2]]. apply ext_eq_symm in H. assert (heq: ext_eq e' (fun _ => CON a)). { apply ext_eq_trans with E; auto. } specialize lbnd_CON_inv with (1:=heq) (2:=H2); intro; subst; constructor. - intros e E H [e' [H0 H2]]. apply ext_eq_symm in H. assert (heq: ext_eq e' (fun x => x)). { apply ext_eq_trans with E; auto. } specialize lbnd_id_inv with (1:=heq) (2:=H2); intro; subst; constructor; lia. - intros e E H [e' [H0 H2]]. apply ext_eq_symm in H. assert (heq: ext_eq e' (fun _ => VAR n)). { apply ext_eq_trans with E; auto. } specialize lbnd_VAR_inv with (1:=heq) (2:=H2); intro; subst; constructor; lia. - intros e'' E H' [e' [H0 H2]]. apply ext_eq_symm in H'. assert (heq: ext_eq e' (fun _ => BND j)). { apply ext_eq_trans with E; auto. } specialize lbnd_BND_inv with (1:=heq) (2:=H2); intro; subst; constructor; lia. - intros e E H H1. apply ext_eq_symm in H. generalize (lbnd_APP_inv f g H H1). intros [s' [t' [H2 [H3 H4]]]]; subst; constructor; auto. + apply IHabst_aux1 with f; auto with Ext_Eq. + apply IHabst_aux2 with g; auto with Ext_Eq. - intros e E H H1. apply ext_eq_symm in H. generalize (lbnd_ABS_inv f H H1). intros [s [H2 H3]]; subst; constructor; auto. apply IHabst_aux with f; auto with Ext_Eq. Qed. (******************************************************************** Properties of newvar and nvC (fresh variables in terms and contexts) ********************************************************************) Lemma greater_newvar_var : forall v:var, newvar (VAR v) > v. Proof. intros; simpl; lia. Qed. Lemma newvar_not_var : forall v:var, ~(newvar (VAR v) = v). Proof. simpl; auto. Qed. Lemma newvar_S : forall (v:var), (newvar (VAR v)) = (S v). Proof. simpl; auto. Qed. Lemma In_VAR_lt_nvC : forall (L:list expr) (v:var), In (VAR v) L -> v < (nvC L). Proof. induction L. - simpl; intros; tauto. - simpl. intros v [H | H]; subst. + rewrite -> newvar_S. generalize (PeanoNat.Nat.max_spec_le (S v) (nvC L)); intros [[H0 H1] | [H0 H1]]; lia. + generalize (PeanoNat.Nat.max_spec_le (newvar a) (nvC L)); intros [[H0 H1] | [H0 H1]]. * rewrite -> H1; auto. * specialize IHL with (1:=H). lia. Qed. Lemma nvC_not_in_context : forall (L:list expr), ~(In (VAR (nvC L)) L). Proof. induction L. - simpl; auto. - intro H; elim IHL. simpl in H. destruct H as [H | H]. rewrite -> H in H. + generalize (PeanoNat.Nat.max_spec_le (newvar a) (nvC L)); intros [[H0 H1] | [H0 H1]]. * rewrite -> H1 in H. rewrite newvar_S in H. assert (h: max (S (nvC L)) (nvC L) = (S (nvC L))). { apply max_l; lia. } rewrite h in H. injection H; lia. * rewrite -> H1 in H. rewrite newvar_S in H. assert (h: max (S (newvar a)) (nvC L) = (S (newvar a))). { apply max_l; lia. } rewrite h in H. injection H; lia. + generalize (PeanoNat.Nat.max_spec_le (newvar a) (nvC L)); intros [[H0 H1] | [H0 H1]]. * rewrite -> H1 in H; auto. * rewrite -> H1 in H; auto. specialize In_VAR_lt_nvC with (1:= H); lia. Qed. Lemma newvar_not_subterm: forall (v:var) (e:expr), v >= (newvar e) -> ~(subterm (VAR v) e). Proof. intros v e; induction e. - simpl; auto; intros H [hp [H0 | H0]]; auto. discriminate H0. - simpl; auto; intros H [hp [H0 | H0]]; auto. injection H0; lia. - simpl; auto; intros H [hp [H0 | H0]]; auto. discriminate H0. - simpl. intros H [hp [H0 | H0]]. + discriminate H0. + assert (Hmax: v >= (newvar e1) /\ v >= (newvar e2)). { generalize (PeanoNat.Nat.le_max_l (newvar e1) (newvar e2)); generalize (PeanoNat.Nat.le_max_r (newvar e1) (newvar e2)); intros H1 H2. split; lia. } destruct Hmax as [H1 H2]. destruct H0 as [H0 | H0]. * generalize (IHe1 H1 H0); auto. * generalize (IHe2 H2 H0); auto. - simpl; intros H [hp [H0 | H0]]. + discriminate H0. + generalize (IHe H H0); auto. Qed. Lemma subterm_lt_nvC : forall (v:var) (l:list expr) (e:expr), subterm (VAR v) e -> In e l -> v < (nvC l). Proof. intro v; induction l; intros e H H0; try tauto. simpl; simpl in H0. generalize (PeanoNat.Nat.le_max_l (newvar a) (nvC l)); generalize (PeanoNat.Nat.le_max_r (newvar a) (nvC l)); intros H1 H2. destruct H0 as [H0 | H0]; subst. - generalize (PeanoNat.Nat.lt_ge_cases v (newvar e)); intros [H0 | H0]; try lia. assert (H0': v >= newvar e); try tauto. specialize newvar_not_subterm with (1:=H0'); tauto. - specialize IHl with (1:=H) (2:=H0); lia. Qed. Lemma subterm_id : forall (e:expr), proper e -> subterm e e. Proof. induction e; simpl; auto. Qed. Hint Resolve subterm_id : hybrid. (******************************************************************** Properties of bv_subst ********************************************************************) Lemma bv_subst_not_occurs : forall (e M:expr) (j:bnd), ~(bv_occurs j e) -> (bv_subst j M e = e). Proof. induction e; simpl; auto. - intros M j H. rewrite <- PeanoNat.Nat.eqb_neq in H. rewrite -> H; auto. - intros M j H. assert (bv1 : ~(bv_occurs j e1)); try tauto. assert (bv2 : ~(bv_occurs j e2)); try tauto. f_equal; auto. - intros M j H; f_equal; auto. Qed. Lemma bv_subst_level : forall (i j:bnd) (e M:expr), level j e -> j <= i -> bv_subst i M e = e. Proof. intros i j e M H. generalize i M; clear i M. induction H; auto. - intros k M H0. simpl. destruct (k =? j) eqn:Hkj; auto. rewrite PeanoNat.Nat.eqb_eq in Hkj; lia. - simpl; intros i0 M H1; f_equal; auto. - simpl; intros i0 M H1; f_equal. apply IHlevel; lia. Qed. Corollary bv_subst_proper : forall (i:bnd) (e M:expr), proper e -> bv_subst i M e = e. Proof. unfold proper; intros; apply bv_subst_level with 0; auto; lia. Qed. Corollary bv_substs_proper : forall (i:bnd) (M:expr) (l:list expr), Forall proper l -> bv_substs i M l = l. Proof. intros i M l; induction l; auto. intro H; simpl. inversion H; subst. f_equal; auto. apply bv_subst_proper; auto. Qed. Lemma bv_subst_abst : forall (E:expr -> expr) (i:bnd), abst i E -> forall (j:bnd) (e e':expr), i < j -> lbnd i E e -> bv_subst j e' e = e. Proof. intros E i [E' [H H0]]. generalize dependent E. generalize H0; intro H0'. induction H0; auto. - intros E H j e e' H1 [E'' [H2 H3]]. rewrite <- H in H2. inversion H3; subst; simpl; auto; try (unfold ext_eq in H2; specialize H2 with (1:=(proper_VAR 0)); inversion H2). destruct (j =? 0) eqn:He; auto. apply (Nat.eqb_eq j 0) in He. lia. - intros E H j e e' H1 [E'' [H2 H3]]. rewrite <- H in H2. inversion H3; subst; simpl; auto; try (unfold ext_eq in H2; specialize H2 with (1:=(proper_VAR 0)); inversion H2). + destruct (j =? i) eqn:He; auto. apply (Nat.eqb_eq j i) in He; lia. + destruct (j =? 0) eqn:He; auto. apply (Nat.eqb_eq j 0) in He; lia. - intros E H j e e' H1 [E'' [H2 H3]]. rewrite <- H in H2. inversion H3; subst; simpl; auto; try (unfold ext_eq in H2; specialize H2 with (1:=(proper_VAR 0)); inversion H2). + destruct (j =? i) eqn:He; auto. apply (Nat.eqb_eq j i) in He; lia. + destruct (j =? 0) eqn:He; auto. apply (Nat.eqb_eq j 0) in He; lia. - intros E H0 j' e' e'' H1 [E'' [H2 H3]]. rewrite <- H0 in H2. inversion H3; subst; simpl; auto; try (unfold ext_eq in H2; specialize H2 with (1:=(proper_VAR 0)); inversion H2). + destruct (j' =? j) eqn:He; auto. apply (Nat.eqb_eq j' j) in He;lia. + destruct (j' =? 0) eqn:He; auto. apply (Nat.eqb_eq j' 0) in He; lia. - intros E H j' e' e'' H1 [E'' [H2 H3]]. rewrite <- H in H2. inversion H3; subst; auto. + unfold ext_eq in H2; specialize H2 with (1:=(proper_VAR 0)); inversion H2. + unfold ext_eq in H2; specialize H2 with (1:=(proper_VAR 0)); inversion H2. + specialize ext_eq_APP_elim1 with (1:=H2); specialize ext_eq_APP_elim2 with (1:=H2); intros H5 H6. simpl. f_equal. * apply IHabst_aux1 with f0; auto with Ext_Eq. ** apply ext_eq_symm; auto. ** unfold lbnd. exists f0; split; auto with Ext_Eq. * apply IHabst_aux2 with g0; auto with Ext_Eq. ** apply ext_eq_symm; auto. ** unfold lbnd. exists g0; split; auto with Ext_Eq. + unfold ext_eq in H2; specialize H2 with (1:=(proper_VAR 0)); inversion H2. + assert (ho:ordinary E''). { apply abst_aux_ordinary with i (fun x : expr => APP (f x) (g x)); auto. } contradiction. - intros E H j' e' e'' H1 [E'' [H2 H3]]. rewrite <- H in H2. inversion H3; subst; auto. + unfold ext_eq in H2; specialize H2 with (1:=(proper_VAR 0)); inversion H2. + unfold ext_eq in H2; specialize H2 with (1:=(proper_VAR 0)); inversion H2. + unfold ext_eq in H2; specialize H2 with (1:=(proper_VAR 0)); inversion H2. + specialize ext_eq_ABS with (1:=H2); intro H5. simpl. f_equal. apply IHabst_aux with f0; auto with Ext_Eq; try lia. * apply ext_eq_symm; auto. * unfold lbnd. exists f0; split; auto with Ext_Eq. + assert (ho:ordinary E''). { apply abst_aux_ordinary with i (fun x : expr => ABS (f x)); auto. } contradiction. Qed. Lemma abst_lbnd_bv_subst : forall (E:expr -> expr) (e e':expr) (i:bnd), abst i E -> proper e' -> lbnd i E e -> E e' = bv_subst i e' e. Proof. intro E. assert (exists n:nat, n=(rank E)). { exists (rank E); auto. } destruct H as [n H]. generalize dependent E. generalize (lt_wf_ind n (fun n => (forall E : expr -> expr, n = rank E -> forall (e e' : expr) (i:bnd), abst i E -> proper e' -> lbnd i E e -> E e' = bv_subst i e' e))). intros H. apply H; auto. clear H n. intros n H E H0 e e' i Ha Hp H1. subst. unfold rank,lbnd in H. unfold lbnd in H1. destruct H1 as [E' [H1 H2]]. inversion H2;subst. - rewrite <- H1;auto. - rewrite <- H1;simpl;auto. assert (h:i=i); auto. rewrite <- Nat.eqb_eq in h. rewrite -> h; auto. - rewrite <- H1;auto. - unfold abst in Ha. rewrite <- H1;auto. destruct Ha as [e'' [H3 H4]]. inversion H4;subst; try (unfold ext_eq in H3; unfold ext_eq in H1; specialize H3 with (1:=(proper_VAR 0)); specialize H1 with (1:=(proper_VAR 0)); rewrite <- H3 in H1; inversion H1). assert (h:i<>j0); try lia. rewrite <- Nat.eqb_neq in h. simpl. rewrite -> h; auto. - simpl. rewrite <- H1; auto. f_equal. + apply H with (size (f (VAR 0)));auto. * rewrite <- H1. ** apply size_APP1;auto. ** apply proper_VAR. * apply abst_app1 with g. unfold abst in Ha. destruct Ha as [e'' [H4 H5]]. unfold abst. exists e'';split;auto. apply ext_eq_trans with E;auto. apply ext_eq_symm;auto. * exists f;split;auto. apply ext_eq_refl. + apply H with (size (g (VAR 0)));auto. * rewrite <- H1. ** apply size_APP2;auto. ** apply proper_VAR. * apply abst_app2 with f. unfold abst in Ha. destruct Ha as [e'' [H4 H5]]. unfold abst. exists e'';split;auto. apply ext_eq_trans with E;auto. apply ext_eq_symm;auto. * exists g;split;auto. apply ext_eq_refl. - simpl. rewrite <- H1; auto. f_equal. apply H with (size (f (VAR 0)));auto. + rewrite <- H1. * apply size_ABS;auto. * apply proper_VAR. + apply abst_abs. unfold abst in Ha. destruct Ha as [e'' [H4 H5]]. unfold abst. exists e'';split;auto. apply ext_eq_trans with E;auto. apply ext_eq_symm;auto. + exists f;split;auto. apply ext_eq_refl. - elim H0. apply ordinary_ext_eq with E. + apply ext_eq_symm;auto. + apply abst_ordinary_ext_eq with i E;auto. apply ext_eq_refl. Qed. Lemma abstr_lbnd_bv_subst : forall (E:expr -> expr) (e e':expr), abstr E -> proper e' -> lbnd 0 E e -> E e' = bv_subst 0 e' e. Proof. unfold abstr; intros; apply abst_lbnd_bv_subst;auto. Qed. Lemma level_bv_subst : forall (i:bnd) (e M:expr), level (i+1) M -> proper e -> level i (bv_subst i e M). Proof. intros i e M; generalize i e; clear i e; induction M; simpl; try constructor; try (inversion H; subst; auto). intros i e H H0. destruct (i =? b) eqn:Hib; auto. - unfold proper in H0; apply level_greater with 0; auto; lia. - inversion H; subst. constructor; auto. apply Nat.eqb_neq in Hib. lia. Qed. Lemma subterm_bv_subst : forall (M e:expr) (i:bnd), bv_occurs i M -> proper e -> subterm e (bv_subst i e M). Proof. intros M; induction M; intros e i H H0; simpl in H; try tauto. - subst. simpl. generalize (PeanoNat.Nat.eqb_refl b); intro H1. rewrite -> H1; auto with hybrid. - simpl; destruct H as [H | H]; auto. - simpl; auto. Qed. Lemma nvC_not_subterm : forall (i:bnd) (l:list expr) (M:expr), In (bv_subst i (VAR (nvC l)) M) l -> bv_occurs i M -> False. Proof. intro i; induction l; try tauto. simpl. generalize (PeanoNat.Nat.le_max_l (newvar a) (nvC l)); generalize (PeanoNat.Nat.le_max_r (newvar a) (nvC l)); intros H1 H2. intros M [H3 | H3] H4. - assert (H2':PeanoNat.Nat.max (newvar a) (nvC l) >= (newvar a)); try tauto. specialize newvar_not_subterm with (1:=H2'); intro H. assert (hp:proper (VAR (PeanoNat.Nat.max (newvar a) (nvC l)))); try apply proper_VAR. specialize subterm_bv_subst with (1:=H4) (2:=hp); intro H0. rewrite <- H3 in H0; auto. - generalize (Nat.max_dec (newvar a) (nvC l)); intros [H | H]. + assert (hp:proper (VAR (PeanoNat.Nat.max (newvar a) (nvC l)))); try apply proper_VAR. specialize subterm_bv_subst with (1:=H4) (2:=hp); intro H0. specialize subterm_lt_nvC with (1:=H0) (2:=H3); intro; lia. + apply IHl with M; auto. rewrite <- H; auto. Qed. Lemma bv_occurs_dec : forall (M:expr) (i:bnd), {bv_occurs i M} + {~(bv_occurs i M)}. Proof. intro M; induction M; auto. - simpl. intro i; apply PeanoNat.Nat.eq_dec. - simpl. intro i; specialize IHM1 with i; specialize IHM2 with i. destruct IHM1 as [ H1 | H1]; destruct IHM2 as [ H2 | H2]; tauto. - simpl. intro i; specialize IHM with (i+1); auto. Qed. (******************************************************************** Properties of fv_subst ********************************************************************) Lemma fv_subst_id : forall (a:expr) (m:var) (e:expr), (newvar a) <= m -> fv_subst m e a = a. Proof. induction a; intros; auto. - simpl in H. assert (H0:false = (m =? v)). { apply not_eq_false_beq; auto. { intros. apply Nat.eqb_eq. symmetry. assumption. } { lia. }} simpl. rewrite <- H0; auto. - simpl. simpl in H. generalize (PeanoNat.Nat.le_max_l (newvar a1) (newvar a2)); generalize (PeanoNat.Nat.le_max_r (newvar a1) (newvar a2)); intros H0 H1. rewrite IHa1; try rewrite IHa2; auto; lia. - simpl. simpl in H. rewrite IHa; auto. Qed. Lemma fv_substs_cxt_lem : forall (s:subst_ty) (a:expr) (l:list expr), In a l -> In (fv_substs s a) (fv_substs_cxt s l). Proof. intros s al; induction l; auto. simpl. intros [H | H]; subst; tauto. Qed. Lemma fv_subst_cxt_cons : forall (m:var) (e:expr) (a:expr) (l:list expr), fv_subst_cxt m e (a::l) = (fv_subst m e a::fv_subst_cxt m e l). Proof. simpl; auto. Qed. Lemma new_fv_subst_cxt : forall (l:list expr) (m:var) (e:expr), (nvC l) <= m -> fv_subst_cxt m e l = l. Proof. induction l; auto. simpl. intros m e H. generalize (PeanoNat.Nat.le_max_r (newvar a) (nvC l)); intro H0. generalize (PeanoNat.Nat.le_max_l (newvar a) (nvC l)); intro H1. f_equal. - apply fv_subst_id; lia. - apply IHl; lia. Qed. (******************************************************************** lbnd is a functional relation ********************************************************************) Lemma lbnd_unique : forall (i:bnd) (e:expr -> expr) (s:expr), lbnd i e s -> forall (t:expr), lbnd i e t -> s = t. Proof. unfold lbnd. intros i e s [e1 [H H1]] t [e2 [H2 H3]]. generalize H2; clear H2. generalize H3; clear H3. generalize t e2; clear t e2. generalize H; clear H. generalize e; clear e. generalize H1; clear H1. generalize i s e1; clear i s e1. intros i s e1; induction 1. - intros e H t e2 H3 H2. assert (ext_eq e2 (fun x:expr => CON a)). { setoid_rewrite -> H2; setoid_rewrite <- H; auto with Ext_Eq. } generalize (lbnd_CON_inv H0 H3); auto. - intros e H t e2 H3 H2. assert (ext_eq e2 (fun x:expr => x)). { setoid_rewrite -> H2; setoid_rewrite <- H; auto with Ext_Eq. } generalize (lbnd_id_inv H0 H3); auto. - intros e H t e2 H3 H2. assert (ext_eq e2 (fun x:expr => VAR n)). { setoid_rewrite -> H2; setoid_rewrite <- H; auto with Ext_Eq. } generalize (lbnd_VAR_inv H0 H3); auto. - intros e H t e2 H3 H2. assert (ext_eq e2 (fun x:expr => BND j)). { setoid_rewrite -> H2; setoid_rewrite <- H; auto with Ext_Eq. } generalize (lbnd_BND_inv H0 H3); auto. - intros e H t0 e2 H3 H2. assert (ext_eq e (fun x : expr => APP (f x) (g x))). { setoid_rewrite <- H; auto with Ext_Eq. } assert (lbnd i e t0). { unfold lbnd; exists e2; auto. } generalize (lbnd_APP_inv f g H0 H1); auto. unfold lbnd; intros [s' [t' [[ef [H4 H5]] [[eg [H6 H7]] H8]]]]. generalize (IHlbnd_aux1 ef (ext_eq_symm H4) s' ef H5 (ext_eq_refl ef)); intro H9. generalize (IHlbnd_aux2 eg (ext_eq_symm H6) t' eg H7 (ext_eq_refl eg)); intro H10. subst; auto. - intros e H t e2 H3 H2. assert (ext_eq e (fun x : expr => ABS (f x))). { setoid_rewrite <- H; auto with Ext_Eq. } assert (lbnd i e t). { unfold lbnd; exists e2; auto. } generalize (lbnd_ABS_inv f H0 H4); auto. unfold lbnd; intros [s' [[e' [H5 H6]] H7]]. generalize (IHlbnd_aux e' (ext_eq_symm H5) s' e' H6 (ext_eq_refl e')); intro. subst; auto. - intros e0 H0 t e2 H3 H2. generalize H; clear H; setoid_rewrite -> H0; setoid_rewrite <- H2; intro H. generalize (lbnd_Err_inv H H3); auto. Qed. (******************************************************************** applying the description theorem to get lbind, a functional version of the lbnd relation ********************************************************************) Definition lbnd_curry : (prodT bnd (expr->expr))->expr->Prop := (uncurry lbnd). Lemma lbnd_curry_eq : forall (i:bnd) (e:expr->expr) (s:expr), (lbnd i e s)=(lbnd_curry (pairT i e) s). Proof. unfold lbnd_curry, uncurry; auto. Qed. Lemma lbnd_curry_total: forall (p:prodT bnd (expr -> expr)), exists s : expr, lbnd_curry p s. Proof. intro p. elim p. unfold lbnd_curry, uncurry. exact lbnd_total. Qed. Lemma lbnd_curry_total_unique : forall (p:prodT bnd (expr -> expr)), exists s : expr, lbnd_curry p s /\ (forall s':expr, lbnd_curry p s' -> s = s'). Proof. intro p. elim p. unfold lbnd_curry, uncurry. intros a b. generalize (lbnd_total a b); intro H. elim H; clear H; intros x H. exists x; split; auto. intros s' H0. generalize (lbnd_unique H H0); auto. Qed. Theorem lbind_exists : exists lbind_curry : (prodT bnd (expr->expr)) -> expr, (forall p:(prodT bnd (expr->expr)), lbnd_curry p (lbind_curry p)). Proof. apply unique_choice. unfold unique; apply lbnd_curry_total_unique. Qed. (******************************************************************** End section hybrid ********************************************************************) Unset Implicit Arguments. End hybrid. Add Parametric Relation (XE:Set) : (expr XE -> expr XE ) ( @ext_eq XE) reflexivity proved by (@ext_eq_refl XE) symmetry proved by (@ext_eq_symm XE) transitivity proved by (@ext_eq_trans XE) as ext_eq_Econ. (******************************************************************** Section lbind ********************************************************************) Section lbind. Hint Resolve ext_eq_refl : Ext_Eq. Set Implicit Arguments. Variable con: Set. Parameter lbind_curry : (prodT bnd (expr con -> expr con)) -> expr con. Axiom lbind_curry_lbnd_curry : forall p:(prodT bnd (expr con->expr con)), lbnd_curry p (lbind_curry p). Definition lbind : bnd -> (expr con -> expr con) -> expr con := curry lbind_curry. Lemma lbind_lbnd : forall i:bnd, forall e:expr con->expr con, lbnd i e (lbind i e). Proof. intros i e. unfold lbind, uncurry. rewrite -> lbnd_curry_eq. apply lbind_curry_lbnd_curry. Qed. Lemma lbind_value : forall i:bnd, forall e:expr con->expr con, forall s:expr con, lbnd i e s -> s = (lbind i e). Proof. intros i e s H. generalize (lbind_curry_lbnd_curry (pairT i e)); intro H0. unfold lbnd_curry, uncurry in H0. apply lbnd_unique with i e; auto. Qed. Lemma abst_lbind_one_to_one : forall (i:bnd) (e: expr con -> expr con), abst i e -> forall (f:expr con -> expr con), abst i f -> lbind i e = lbind i f -> ext_eq e f. Proof. intros i e H f H0 H1. generalize (lbind_lbnd i e); rewrite H1; intro H2. generalize (lbind_lbnd i f); intro H3. apply abst_lbnd_one_to_one with i (lbind i f); auto. Qed. Lemma lbind_ext_eq : forall (i:bnd) (e e' : expr con -> expr con), (ext_eq e e') -> (lbind i e)=(lbind i e'). Proof. intros i e e' h1. generalize (lbind_lbnd i e); generalize (lbind_lbnd i e'); intros h2 h3. specialize lbnd_ext_eq with (1:=h1) (2:=h3); intro h4. apply lbnd_unique with i e'; auto. Qed. (******************************************************************** rewrite rules for lbind ********************************************************************) Lemma lbind_CON : forall (i:bnd) (a:con), (lbind i (fun x => CON a))=(CON a). Proof. intros i a; symmetry; apply lbind_value. unfold lbnd. exists (fun x:expr con => CON a); split; auto with Ext_Eq. apply lbnd_CON; auto. Qed. Lemma lbind_CON_ext_eq : forall (i:bnd) (a:con) (B:expr con -> expr con), ext_eq B (fun x => CON a) -> lbind i B = CON a. Proof. intros i a B H; symmetry; apply lbind_value. unfold lbnd. exists (fun x:expr con => CON a); split; auto with Ext_Eq. - apply ext_eq_symm; auto. - apply lbnd_CON; auto. Qed. Lemma lbind_id : forall (i:bnd), (lbind i (fun x => x))=(BND con i). Proof. intro i; symmetry; apply lbind_value. unfold lbnd. exists (fun x:expr con => x); split; auto with Ext_Eq. apply lbnd_id; auto. Qed. Lemma lbind_VAR : forall (i:bnd) (n:var), (lbind i (fun x => VAR con n))=(VAR con n). Proof. intros i n; symmetry; apply lbind_value. unfold lbnd. exists (fun x:expr con => VAR con n); split; auto with Ext_Eq. apply lbnd_VAR; auto. Qed. Lemma lbind_BND : forall (i j:bnd), (lbind i (fun x => BND con j))=(BND con j). Proof. intros i j; symmetry; apply lbind_value. unfold lbnd. exists (fun x:expr con => BND con j); split; auto with Ext_Eq. apply lbnd_BND; auto. Qed. Lemma lbind_APP : forall (i:bnd) (f g: expr con -> expr con), (lbind i (fun x => APP (f x) (g x)))=(APP (lbind i f) (lbind i g)). Proof. intros i f g. generalize (lbind_lbnd i f); generalize (lbind_lbnd i g); unfold lbnd. intros [eg [H H0]] [ef [H1 H2]]. symmetry; apply lbind_value. unfold lbnd. exists (fun x: expr con => APP (ef x) (eg x)); split. - unfold ext_eq in H; unfold ext_eq in H1; unfold ext_eq; intros x h1. rewrite (H x h1); rewrite (H1 x h1); auto. - apply lbnd_APP; auto. Qed. Lemma lbind_ABS : forall (i:bnd) (f: expr con -> expr con), (lbind i (fun x => ABS (f x)))=(ABS (lbind (i+1) f)). Proof. intros i f. generalize (lbind_lbnd (i+1) f); unfold lbnd. intros [ef [H H0]]. symmetry; apply lbind_value. unfold lbnd. exists (fun x: expr con => ABS (ef x)); split. - unfold ext_eq in H; unfold ext_eq; intros x h1. rewrite (H x h1); auto. - apply lbnd_ABS; auto. Qed. Hint Rewrite lbind_CON lbind_id lbind_VAR lbind_BND lbind_APP lbind_ABS : lbind_rw. (******************************************************************** Properties of substitution and lbind ********************************************************************) Lemma abstr_lbind_bv_subst : forall (E:expr con -> expr con) (e:expr con), abstr E -> proper e -> (E e) = bv_subst 0 e (lbind 0 E). Proof. intros E e H H0. apply abstr_lbnd_bv_subst;auto. apply lbind_lbnd. Qed. Hint Rewrite lbind_CON lbind_id lbind_VAR lbind_BND lbind_APP lbind_ABS : lbind_rw. Lemma abstr_bv_subst_lbind : forall (A:expr con -> expr con) (i:bnd), abst_aux i A -> forall (j:bnd) (e:expr con), i <= j -> bv_subst j e (ABS (lbind i A)) = ABS (lbind i A). Proof. intros A i; induction 1. - autorewrite with lbind_rw; simpl; auto. - autorewrite with lbind_rw; simpl. intros j e H. assert (h0: j+1 <>i); try lia. assert (h1: j+1 =? i = false). { rewrite not_eq_false_beq with nat Nat.eqb (j+1) i; auto. intros. apply Nat.eqb_eq. symmetry. assumption. } rewrite h1; auto. - autorewrite with lbind_rw; simpl; auto. - autorewrite with lbind_rw; simpl; intros j' e' H0. assert (h0: j'+1 <>j); try lia. assert (h1: j'+1 =? j = false). { rewrite not_eq_false_beq with nat Nat.eqb (j'+1) j; auto. intros. apply Nat.eqb_eq. symmetry. assumption. } rewrite h1; auto. - autorewrite with lbind_rw; simpl; intros j e H1. simpl in IHabst_aux1. simpl in IHabst_aux2. specialize (IHabst_aux1 j e H1). specialize (IHabst_aux2 j e H1). injection IHabst_aux1; injection IHabst_aux2; intros H2 H3. rewrite -> H2; rewrite -> H3; auto. - intros j e H0. simpl. autorewrite with lbind_rw. f_equal. apply IHabst_aux; auto; lia. Qed. (******************************************************************** lambda and injectivity ********************************************************************) Definition lambda : (expr con -> expr con) -> expr con := fun e:expr con -> expr con => (ABS (lbind 0 e)). Lemma abstr_lbind_simp_aux : forall (i:bnd)(e:expr con->expr con), (abst_aux i e) -> forall (f:expr con->expr con), (abst_aux i f) -> (lbind i e)=(lbind i f) -> e=f. Proof. intros i e; induction 1. - intro f; destruct 1; try (autorewrite with lbind_rw; discriminate 1). autorewrite with lbind_rw; intro H; rewrite H; auto. - intro f; destruct 1; try (autorewrite with lbind_rw; discriminate 1). + auto. + rewrite lbind_id; rewrite lbind_BND; inversion 1. subst. generalize (Nat.lt_irrefl j); intro H1; elim H1; auto. - intro f; destruct 1; try (autorewrite with lbind_rw; discriminate 1). autorewrite with lbind_rw; intro H; rewrite H; auto. - intro f; destruct 1; try (autorewrite with lbind_rw; discriminate 1). + rewrite lbind_id; rewrite lbind_BND; inversion 1. subst. generalize (Nat.lt_irrefl i); intro H1; elim H1; auto. + rewrite lbind_BND; rewrite lbind_BND; inversion 1; auto. - intro f0; destruct 1; try (autorewrite with lbind_rw; discriminate 1). autorewrite with lbind_rw; inversion 1. generalize (IHabst_aux1 f0 H1_ H3); generalize (IHabst_aux2 g0 H1_0 H4); intros; subst; auto. - intro f0; destruct 1; try (autorewrite with lbind_rw; discriminate 1). autorewrite with lbind_rw; inversion 1. generalize (IHabst_aux f0 H0 H3); intro; subst; auto. Qed. Lemma abstr_lbind_simp : forall (i:bnd)(e:expr con->expr con), (abst i e) -> forall (f:expr con->expr con), (abst i f) -> (lbind i e)=(lbind i f) -> (ext_eq e f). Proof. intros i e [e' [H H0]] f [f' [H1 H2]] H3. apply abst_lbind_one_to_one with i; auto. - unfold abst; exists e'; split; auto with Ext_Eq. - unfold abst; exists f'; split; auto with Ext_Eq. Qed. Lemma abstr_lam_simp : forall e f:expr con->expr con, (abstr e) -> (abstr f) -> (lambda e)=(lambda f) -> (ext_eq e f). Proof. unfold lambda; intros e f H H0 H1. inversion H1. apply abstr_lbind_simp with 0; auto. Qed. Lemma abstr_lam_simp_eta : forall e f:expr con->expr con, (abstr e) -> (abstr f) -> (lbind 0 (fun x => e x))=(lbind 0 (fun x => f x)) -> (ext_eq e f). Proof. intros e f h1 h2 h3. generalize (ext_eq_eta e); generalize (ext_eq_eta f); intros h4 h5. generalize (lbind_ext_eq 0 h4); intro h6. generalize (lbind_ext_eq 0 h5); intro h7. apply abstr_lam_simp; auto. unfold lambda; auto. rewrite -> h7; rewrite -> h3; rewrite h6; auto. Qed. (******************************************************************** Other properties ********************************************************************) Lemma lbind_does_not_occur : forall (y:expr con) (i:bnd), (lbind i (fun x => y))=y. Proof. induction y; intro i; autorewrite with lbind_rw; auto. - rewrite IHy1; rewrite IHy2; auto. - generalize (lbind_ABS i (fun x => y)); intro H. rewrite IHy; auto. Qed. Lemma level_lbnd_abst : forall (i:bnd) (E1:expr con), (level i E1) -> forall (j:bnd), j+1=i -> exists E2:expr con->expr con, (lbnd_aux j E2 E1 /\ abst_aux j E2). Proof. intros i E1; induction 1. - intros j h; exists (fun x:expr con => (CON a)); split. + apply lbnd_CON. + apply abst_CON. - intros j h; exists (fun x:expr con => (VAR con n)); split. + apply lbnd_VAR. + apply abst_VAR. - intros k h. subst. assert (S k > j); try lia. apply Nat.succ_le_mono in H0. apply Nat.lt_eq_cases in H0. destruct H0 as [h | h]. + exists (fun x:expr con => (BND con j)); split. * apply lbnd_BND; auto. * apply abst_BND; auto. + subst. exists (fun x:expr con => x); split. * apply lbnd_id. * apply abst_id. - intros j h. elim (IHlevel1 j h); elim (IHlevel2 j h). intros E2 [h1 h2] E3 [h3 h4]. exists (fun x => (APP (E3 x) (E2 x))); split. + apply lbnd_APP; auto. + apply abst_APP; auto. - intros j h. assert (j+1+1=i+1); try lia. elim (IHlevel (j+1) H0); intros E2 [h1 h2]. exists (fun x => (ABS (E2 x))); split. + apply lbnd_ABS; auto. + apply abst_ABS; auto. Qed. Lemma level_lbind_abst : forall (i:bnd) (E1:expr con), (level i E1) -> forall (j:bnd), j+1=i-> exists E2:expr con->expr con, (lbind j E2=E1 /\ abst j E2). Proof. intros i E1 h1 j h2. generalize (level_lbnd_abst h1 j h2); intros [E2 [h3 h4]]. assert (lbnd j E2 E1). { unfold lbnd; exists E2. split; auto with Ext_Eq. } generalize (lbind_value H); intro; subst. exists E2; split; auto. unfold abst; exists E2; auto with Ext_Eq. Qed. Lemma level_lbnd_abst_j : forall (j:bnd) (E1:expr con), (level j E1) -> exists E2:expr con->expr con, (lbnd_aux j E2 E1 /\ abst_aux j E2). Proof. intros j E1; induction 1. - exists (fun x:expr con => (CON a)); split; [apply lbnd_CON | apply abst_CON]. - exists (fun x:expr con => (VAR con n)); split; [apply lbnd_VAR | apply abst_VAR]. - exists (fun x:expr con => (BND con j)); split; [apply lbnd_BND | apply abst_BND]; auto. - elim IHlevel1; elim IHlevel2. intros E2 [h1 h2] E3 [h3 h4]. exists (fun x => (APP (E3 x) (E2 x))); split. + apply lbnd_APP; auto. + apply abst_APP; auto. - elim IHlevel; intros E2 [h1 h2]. exists (fun x => (ABS (E2 x))); split. + apply lbnd_ABS; auto. + apply abst_ABS; auto. Qed. Lemma level_lbind_abst_j : forall (j:bnd) (E1:expr con), (level j E1) -> exists E2:expr con->expr con, (lbind j E2=E1 /\ abst j E2). Proof. intros j E1 h1. generalize (level_lbnd_abst_j h1); intros [E2 [h3 h4]]. assert (lbnd j E2 E1). - unfold lbnd; exists E2. split; auto with Ext_Eq. - generalize (lbind_value H); intro; subst. exists E2; split; auto. unfold abst; exists E2; auto with Ext_Eq. Qed. Lemma proper_lambda_abstr : forall E1:expr con, proper (ABS E1) -> exists E2:expr con->expr con, ((ABS E1)=(lambda E2) /\ (abstr E2)). Proof. unfold lambda, proper, abstr. intros E1 h. inversion h; subst. assert (0+1=0+1); try lia. generalize (level_lbind_abst H1 0 H); intros [E2 [h1 h2]]. exists E2; split; auto. rewrite <- h1; auto. Qed. Lemma proper_lambda : forall E1:expr con, proper (ABS E1) -> exists E2:expr con->expr con, (ABS E1)=(lambda (fun x => E2 x)). Proof. unfold lambda, proper. intros E1 H. inversion H; subst. generalize level_lbnd_aux; intro H0. generalize (H0 con 0 E1 H2); clear H0; intro H0. elim H0; clear H0; intros E2 H0. exists E2. assert (lbnd 0 E2 E1). { unfold lbnd. exists E2; split; auto with Ext_Eq. } assert (lbnd 0 (fun x => E2 x) E1). { apply lbnd_ext_eq with E2. apply ext_eq_eta. unfold lbnd. exists E2; split; auto with Ext_Eq. } generalize (lbind_value H3); intro H4. subst; auto. Qed. Lemma level_lbind_eta_e : forall (i:bnd) (E:expr con->expr con), abst i E -> level (i+1) (lbind i (fun x => E x)) -> forall (x:expr con), proper x -> level i x -> (level i (E x)). Proof. intros i E [e' [H H0]]. generalize E H; clear E H. induction H0. (* CON case *) - intros E H H0 x h1 H1. rewrite <- H; auto. apply level_CON; auto. (* id case *) - intros E H H0 x h1 H1. rewrite <- H; auto. (* VAR case *) - intros E H H0 x h1 H1. rewrite <- H; auto. apply level_VAR; auto. (* BND case *) - intros E H' H1 x h1 H2. rewrite <- H'; auto. apply level_BND; auto. (* APP case *) - intros E H H0 x h1 H1. rewrite <- H; auto. generalize (lbind_lbnd i (fun x => E x)); intro H2. assert (ext_eq (fun x => E x) (fun x => APP (f x) (g x))). { apply ext_eq_trans with E; auto with Ext_Eq. apply ext_eq_symm; auto. } generalize (lbnd_APP_inv (fun x => f x) (fun x => g x) H3 H2). intros [s [t [H4 [H5 H6]]]]. rewrite H6 in H0. inversion H0; subst. apply level_APP; auto. + apply IHabst_aux1; auto with Ext_Eq. generalize (lbind_value H4); intro; subst; auto. + apply IHabst_aux2; auto with Ext_Eq. generalize (lbind_value H5); intro; subst; auto. (* ABS case *) - intros E H H0' x h1 H1. rewrite <- H; auto. generalize (lbind_lbnd i (fun x => E x)); intro H2. assert (ext_eq (fun x => E x) (fun x => ABS (f x))). { apply ext_eq_trans with E; auto with Ext_Eq. apply ext_eq_symm; auto. } generalize (lbnd_ABS_inv (fun x => f x) H3 H2). intros [s [H4 H5]]. rewrite H5 in H0'. inversion H0'; subst. apply level_ABS; auto. apply IHabst_aux; auto with Ext_Eq. + generalize (lbind_value H4); intro; subst; auto. + apply level_succ; auto. Qed. Lemma abst_level_lbind : forall (i:bnd) (E:expr con -> expr con), abst i E -> level (i+1) (lbind i E). Proof. intros i E H. generalize (lbind_lbnd i E); intro H0. apply abst_lbnd_level with E; auto. Qed. Lemma level_lbind_e : forall (i:bnd) (E:expr con->expr con), abst i E -> level (i+1) (lbind i E) -> forall (x:expr con), proper x -> level i x -> (level i (E x)). Proof. intros i E [e' [H H0]]. generalize E H; clear E H. induction H0. (* CON case *) - intros E H H0 x h1 H1. rewrite <- H; auto. apply level_CON; auto. (* id case *) - intros E H H0 x h1 H1. rewrite <- H; auto. (* VAR case *) - intros E H H0 x h1 H1. rewrite <- H; auto. apply level_VAR; auto. (* BND case *) - intros E H' H1 x h1 H2. rewrite <- H'; auto. apply level_BND; auto. (* APP case *) - intros E H H0 x h1 H1. rewrite <- H; auto. generalize (lbind_lbnd i E); intro H2. assert (ext_eq E (fun x => APP (f x) (g x))). { apply ext_eq_symm; auto. } generalize (lbnd_APP_inv f g H3 H2). intros [s [t [H4 [H5 H6]]]]. rewrite H6 in H0. inversion H0; subst. apply level_APP; auto. + apply IHabst_aux1; auto with Ext_Eq. generalize (lbind_value H4); intro; subst; auto. + apply IHabst_aux2; auto with Ext_Eq. generalize (lbind_value H5); intro; subst; auto. (* ABS case *) - intros E H H0' x h1 H1. rewrite <- H; auto. generalize (lbind_lbnd i E); intro H2. assert (ext_eq E (fun x => ABS (f x))). { apply ext_eq_symm; auto. } generalize (lbnd_ABS_inv f H3 H2). intros [s [H4 H5]]. rewrite H5 in H0'. inversion H0'; subst. apply level_ABS; auto. apply IHabst_aux; auto with Ext_Eq. + generalize (lbind_value H4); intro; subst; auto. + apply level_succ; auto. Qed. Lemma abstr_proper: forall E:expr con -> expr con, (abstr E) -> (proper (lambda E)). Proof. unfold abstr,proper,lambda. intros E [E' [h1 h2]]. apply level_ABS. change (level 1 (lbind 0 E)). generalize (lbind_ext_eq 0 h1); intro h3. rewrite <- h3. clear h1 h3. generalize h2; clear h2; induction 1. - rewrite lbind_CON; apply level_CON. - rewrite lbind_id; apply level_BND; auto with arith. - rewrite lbind_VAR; apply level_VAR. - rewrite lbind_BND; apply level_BND; auto with arith. - rewrite lbind_APP; apply level_APP; auto. - rewrite lbind_ABS; apply level_ABS; auto. Qed. Lemma abstr_proper_e : forall (E:expr con -> expr con) (e':expr con), abstr E -> proper e' -> (proper (E e')). Proof. intros E e' h1 h2. generalize (abstr_proper h1); intro h3. unfold proper,lambda in h3. inversion h3; subst; clear h3. unfold proper. apply level_lbind_e; auto. Qed. Lemma abstr_size_lbind : forall E:expr con -> expr con, abstr E -> forall (i:bnd) (j:var), (size (lbind i E))=(size (E (VAR con j))). Proof. intros E [E' [h1 h2]]. generalize h2 E h1; clear h1 h2 E. induction 1. - intros E h1 j n. generalize (lbind_ext_eq j h1); intro h2. rewrite <- h2. rewrite <- h1; auto. + autorewrite with lbind_rw; auto. + apply proper_VAR; auto. - intros E h1 j n. generalize (lbind_ext_eq j h1); intro h2. rewrite <- h2. rewrite <- h1. + autorewrite with lbind_rw; auto. + apply proper_VAR; auto. - intros E h1 j n'. generalize (lbind_ext_eq j h1); intro h2. rewrite <- h2. rewrite <- h1. + autorewrite with lbind_rw; auto. + apply proper_VAR; auto. - intros E h1 k n. generalize (lbind_ext_eq k h1); intro h2. rewrite <- h2. rewrite <- h1. + autorewrite with lbind_rw; auto. + apply proper_VAR; auto. - intros E h1 j n. generalize (lbind_ext_eq j h1); intro h2. rewrite <- h2. rewrite <- h1. + autorewrite with lbind_rw. simpl. assert (h3: (size (lbind j f) = size (f (VAR con n)))). { apply IHh2_1; auto with Ext_Eq. } assert (h4: (size (lbind j g) = size (g (VAR con n)))). { apply IHh2_2; auto with Ext_Eq. } rewrite h3; rewrite h4; auto. + apply proper_VAR; auto. - intros E h1 j n. generalize (lbind_ext_eq j h1); intro h3. rewrite <- h3. rewrite <- h1. + autorewrite with lbind_rw. simpl. assert (h4: (size (lbind (j+1) f) = size (f (VAR con n)))). { apply IHh2; auto with Ext_Eq. } rewrite h4; auto. + apply proper_VAR; auto. Qed. Theorem eq_ext_double: forall (f g: expr con -> expr con -> expr con), (forall x, proper x -> abstr (f x)) -> (forall x, proper x -> abstr (g x)) -> abstr (fun x => lambda (f x)) -> abstr (fun x => lambda (g x)) -> lbind 0 (fun x => lambda (f x)) = lbind 0 (fun x => lambda (g x)) -> forall x1, proper x1 -> ext_eq (f x1) (g x1). Proof. intros f g H H0 H1 H2 H3 x1 H4. apply abst_lbind_one_to_one with 0; unfold abstr in H,H0; auto. apply abstr_lbind_simp in H3; unfold abstr in H,H0; auto. unfold ext_eq in H3. apply H3 in H4. unfold lambda in H4. inversion H4. auto. Qed. (******************************************************************** proper_VAR_induct ********************************************************************) Theorem proper_VAR_induct : forall (P:expr con -> Prop) (e:expr con), proper e -> (forall a:con, P (CON a)) -> (forall n:var, P (VAR con n)) -> (forall E1 E2:expr con, proper E1 -> proper E2 -> P E1 -> P E2 -> P (APP E1 E2)) -> (forall E:expr con -> expr con, abstr E -> forall n:var, P (E (VAR con n)) -> P (lambda E)) -> P e. Proof. intros P e H H0 H1 H2 H3. assert (exists i:nat, i=(size e)). { exists (size e); auto. } elim H4; clear H4; intros i H4. generalize (lt_wf_ind i (fun j:nat => (forall e: expr con, (j=(size e) -> (proper e) -> P e)))). intro H5; apply H5; clear H5; auto. clear H4 i H e. intros n H e H4 H5. induction e. - apply H0. - apply H1. - absurd (proper (BND con b)); auto. apply bnd_not_proper; auto. - generalize (proper_APP1 H5); generalize (proper_APP2 H5); intros h1 h2. assert ((size e1) < n). { generalize (size_APP1 e1 e2); intro; lia. } assert ((size e2) < n). { generalize (size_APP2 e1 e2); intro; lia. } assert (size e1=size e1); auto. assert (size e2=size e2); auto. generalize (H (size e1) H6 e1 H8 h2); intro h3. generalize (H (size e2) H7 e2 H9 h1); intro h4. apply H2; auto. - generalize (proper_lambda_abstr H5); intros [E2 [h1 h2]]. rewrite h1; rewrite h1 in H5; rewrite h1 in H4. apply H3 with 0; auto. apply H with (n-1); try lia; auto. generalize (size_positive (lambda E2)); subst; lia. + simpl in H4. rewrite <- (abstr_size_lbind h2 0 0). lia. + apply abstr_proper_e; auto. apply proper_VAR. Qed. End lbind. (******************************************************************** Properties useful for OLs (part of the eventual API of Hybrid) ********************************************************************) Section api. Hint Resolve ext_eq_refl : api. Hint Resolve level_CON level_VAR level_BND level_APP level_ABS : api. Hint Resolve proper_APP abstr_proper : api. Hint Unfold proper : api. Hint Rewrite ext_eq_eta : api. Variable con: Set. Lemma abstr_level0: forall E:expr con -> expr con, (abstr E) -> (level 0 (lambda E)). Proof. apply abstr_proper. Qed. Lemma abst_i_id : forall (i:bnd), abst i (fun x:expr con => x). Proof. unfold abst; intros i. exists (fun x => x); split; auto; try constructor. Qed. Lemma abst_con : forall (i:bnd) (c:con), abst i (fun x => (CON c)). Proof. unfold abst; intros i c. exists (fun x => (CON c)); split; auto with api. constructor. Qed. Lemma abst_app : forall (i:bnd) (e1 e2:expr con -> expr con), abst i e1 -> abst i e2 -> abst i (fun x => APP (e1 x) (e2 x)). Proof. unfold abst; intros i e1 e2 [e1' [H H0]] [e2' [H1 H2]]. exists (fun x => (APP (e1' x) (e2' x))); split; auto. - unfold ext_eq; intros x H3. rewrite -> H; try rewrite -> H1; auto. - constructor; auto. Qed. Hint Resolve abst_i_id abst_con abst_app : api. Hint Unfold abstr : api. Lemma abstr_id : abstr (fun x:expr con => x). Proof. auto with api. Qed. Lemma abstr_con : forall (c:con), abstr (fun x => (CON c)). Proof. auto with api. Qed. Lemma abstr_app : forall (e1 e2:expr con -> expr con), abstr e1 -> abstr e2 -> abstr (fun x => APP (e1 x) (e2 x)). Proof. auto with api. Qed. Lemma abstr_lambda : forall (e:expr con -> expr con), abstr e -> abstr (fun _ => (lambda e)). Proof. intros e H. apply proper_abstr. apply abstr_proper; auto. Qed. Lemma lbindEq : forall (FX FX':expr con -> expr con), abstr FX -> abstr FX' -> lbind 0 FX = lbind 0 FX' -> ext_eq FX FX'. Proof. intros FX FX' H H0 H1. apply abstr_lbind_simp with 0; auto. Qed. Lemma exprInhabited: exists x: expr con, proper x. Proof. exists (VAR con 0); auto with api. Qed. End api. #[global] Hint Resolve ext_eq_refl : hybrid. #[global] Hint Resolve proper_APP abstr_proper : hybrid. #[global] Hint Resolve ext_eq_eta : hybrid. #[global] Hint Resolve level_CON level_VAR level_BND level_APP level_ABS : hybrid. #[global] Hint Resolve proper_APP abstr_proper abstr_level0 : hybrid. #[global] Hint Unfold proper: hybrid. #[global] Hint Resolve abstr_id abstr_con abstr_app : hybrid. #[global] Hint Resolve lbindEq exprInhabited : hybrid. (* May be needed in sections: Hint Rewrite ext_eq_eta : hybrid. *)