proposition: Lemma demo_ereplace_working : forall (P:nat->nat->Prop) x y, (forall n, P n n) -> (x > 0 -> x = y) -> (x > 0) -> P x y.
proof: Proof. Proof using. introv H E L. dup 4. try apply H. eapply equates_2. apply H. auto. eapply equates_2; eauto. equates 2. demo. demo. Abort. Lemma demo_equates_non_dep : forall (P:nat->nat->nat->Prop) x y z, P x y z. Proof using. intros. dup 6. equates 1. demo. demo. equates 2. demo. demo. equates 3. demo. demo. equates 1 2. demo. demo. demo. equates (>> 1 2). demo. demo. demo. Abort. Lemma demo_equates_dep : forall (P:nat->forall A, A->Prop) x (T:Type) z, P x T z. Proof using. intros. dup 4. equates 1. demo. demo. try equates 2. equates 3. demo. demo. equates 1 3. demo. demo. demo. Abort. Lemma demo_applys_eq : forall (P:nat->nat->nat->Prop) x x' y y' z z', (P x y z -> P x y z') /\ (P x y z -> P x' y z) /\ (P x y z -> P x' y' z) /\ (P x y z -> P x' y' z'). Proof using. intros. splits; intros M. { applys_eq_core M. demo. } { applys_eq_core M. demo. } { applys_eq_core M. demo. demo. } { applys_eq_core M. demo. demo. demo. } Abort. Lemma demo_applys_eq_dep : forall (P:forall A, A->nat->Prop) T x x' y y', (P T x y-> P T x y') /\ (P T x y -> P T x' y) /\ (P T x y -> P T x' y'). Proof using. intros. splits; intros M. { applys_eq_core M. demo. } { applys_eq_core M. demo. } { applys_eq_core M. demo. demo. } Abort. Lemma demo_applys_eq_dep_middle : forall (P:nat->forall A, A->Prop) x x' (T:Type) y y', (P x T y -> P x T y') /\ (P x T y -> P x' T y) /\ (P x T y -> P x' T y'). Proof using. intros. splits; intros M. { applys_eq_core M. demo. } { applys_eq_core M. demo. } { applys_eq_core M. demo. demo. } Abort. Section IndHeight. Inductive trm : Type := | trm_var : nat -> trm | trm_abs : nat -> trm -> trm | trm_app : trm -> trm -> trm. Parameter subst : nat -> trm -> trm -> trm. Inductive bigred : trm -> trm -> Prop := | bigred_val : forall v, bigred v v | bigred_abs : forall x t, bigred (trm_abs x t) (trm_abs x t) | bigred_app : forall t1 t2 x t3 v2 v, bigred t1 (trm_abs x t3) -> bigred t2 v2 -> bigred (subst x v2 t3) v -> bigred (trm_app t1 t2) v. Inductive bigredh : nat -> trm -> trm -> Prop := | bigredh_val : forall n v, bigredh (S n) v v | bigredh_abs : forall n x t, bigredh (S n) (trm_abs x t) (trm_abs x t) | bigredh_app : forall n t1 t2 x t3 v2 v, bigredh n t1 (trm_abs x t3) -> bigredh n t2 v2 -> bigredh n (subst x v2 t3) v -> bigredh (S n) (trm_app t1 t2) v. Hint Extern 1 ((_ < _)%nat) => lia. Hint Constructors bigred bigredh. Lemma bigredh_lt : forall n n' t v, bigredh n t v -> (n < n')%nat -> bigredh n' t v. Proof using. introv H. gen n'. induction H; introv L; (destruct n' as [|n']; [ false; lia | autos* ]). Qed.
imports: TLC(LibTactics) Coq.micromega.Lia