Library TLC.LibTacticsDemos

Set Implicit Arguments.
From TLC Require Import LibTactics.
Require Import Coq.omega.Omega.

Definitions used in demos

Parameter H1 H2 H3 H4 H5 H6 : Prop.

Assertions, cuts, contradiction

Lemma demo_false_1 :
  forall (n:nat), (forall m, m = n -> False ) -> H1.
Proof using.
  intros n P. dup 5.
  false. eapply P. reflexivity.
  false (P n (refl_equal n)).
  false P. reflexivity.
  false*.
  lets: (P n). false.
Qed.

Lemma demo_false_2 :
  0 = 1 -> 1 = 2.
Proof using.
  intros. dup 3.
  try contradiction. demo.
  discriminate.
  false.
Qed.

Lemma demo_false_3 :
  (forall b, b = false ) -> False.
Proof using.
  introv H. dup.
  false (>> H true).
  false H true.
Qed.

Lemma demo_tryfalse :
  forall n, S n = 1 -> n = 0.
Proof using.
  intros. dup 2.
  destruct n. auto. false.
  destruct n; tryfalse. auto.
Qed.

Lemma demo_asserts_cuts :
  True.
Proof using.
  dup 7.
  asserts U: H2. demo. demo.
  asserts [U V]: (H2 /\ H3). demo. demo.
  asserts U V W: (H2 /\ H3 /\ H4). demo. demo.
  asserts x y E F: (exists x y, S x = y /\ x > 0). demo. demo.
  asserts: (H2 /\ H3). demo. demo.
  asserts~ U: (0 = 0). demo.
  cuts U V: (H2 /\ H3). demo. demo.
Qed.

Assumptions

Lemma demo_lets :
  (H1 -> H2 -> H3 /\ H4 ) -> (H1 -> H2 ) -> H1 -> H3.
Proof using.
  intros P Q R.
  lets U: (Q R).
  lets [V W]: (P R U).
  lets V1 W1: (P R U).
  lets: (P R).
  lets U': U.
  demo.
Qed.

Apply

Definition Dup x := x + x.

Lemma demo_applys : forall P : (nat -> nat ) -> nat -> Prop,
  (forall f, P f (f 0)) -> P Dup 0.
Proof using.
  intros. dup 4.
  apply (H Dup).
  apply H.
  refine (H _).
  applys H.
Qed.

Lemma demo_applys_to :
  (H1 -> H2 -> H3 /\ H4 ) -> (H1 -> H2 ) -> H1 -> H3.
Proof using.
  introv P Q R. dup.
  applys_to R Q. demo.
  applys_to R P. demo.
Qed.

Introduction

Section IntrovTest.

Variables P1 P2 P3 : nat -> Prop.

Lemma demo_introv_1 :
  forall a b, P1 a -> P2 b -> forall c d, P3 c -> P1 d -> c = b.
Proof using.
  dup 4.
  introv.
  introv. demo.
  introv A. introv B. introv. intros C D. demo.
  introv A B. introv. demo.
  introv A B C D. demo.
Qed.

Definition Same (x y : nat) := True -> x = y.
Definition Sym (x:nat) := forall y, x = y -> Same y x.

Lemma demo_introv_2 :
  forall a, Sym a.
Proof using.
  dup 4.
  introv.
  introv. demo.
  introv E. introv F. demo.
  introv E F. demo.
  introv E. introv. demo.
Qed.

Lemma demo_introv_3 :
  forall a, a = 0 -> Sym a.
Proof using.
  dup 5.   introv. demo.
  introv E. demo.
  introv E F. demo.
  introv E F G. demo.
  try (introv E F G H). demo.
Qed.

Definition TestSym := (forall a, a = 0 -> Sym a).

Lemma demo_introv_4 :
  TestSym.
Proof using.
  dup 2.   introv. demo.
  introv E. demo.
Qed.

Lemma demo_introv_5 :
  forall a, a = 0 -> ~ Sym a.
Proof using.
  dup 2.   introv E. demo.
  introv E F. demo.
Qed.

Definition AllSameAs (x:nat) := forall y, Same y x.
Definition AllSame := forall x, AllSameAs x.

Lemma demo_introv_6 :
  AllSame.
Proof using.
  dup 2.
  introv. introv. demo.
  introv E. demo.
Qed.

Definition AllSameAgain := AllSame.

Lemma demo_introv_7 :
  AllSameAgain.
Proof using.
  dup 2.
  introv. introv. demo.
  introv E. demo.
Qed.

Lemma demo_introv_8 :
  forall a (c:nat) b, P1 a -> P2 b -> True.
Proof using.
  introv c E F. demo.
Qed.

Definition IMP P A (x y : A) := P -> x = y.

Lemma demo_intros_all :
     (forall a b, P1 a -> P2 b -> IMP H1 a b )
  /\ (forall a b, a = 0 -> b = 1 -> ~ (a = b )).
Proof using.
  split.
  intros_all. demo.
  intros_all. demo.
Qed.

Definition testing f :=
  forall (x:nat), f x -> True.

Lemma demo_introv_what_to_do : testing (fun a => a = 0).
Proof using.
  dup.
    intro. demo.     hnf. intro. demo. Qed.

End IntrovTest.

Arrow Introduction

Section ArrowTest.

Parameters P1 P2 P3 : nat -> Prop.

Lemma demo_arrow_1 :
  forall a b, P1 a -> P2 b -> forall c d, P3 c -> P1 d -> c = b.
Proof using.
  dup 4.
  =>>.
  =>>. demo.
  =>> A. =>> B. =>>. =>> C D. demo.
  =>> A B. =>>. demo.
  =>> A B. =>>. =>> C D. demo.
Qed.

Lemma demo_arrow_2 :
  forall a, Sym a.
Proof using.
  dup 4.
  =>>.
  =>>. demo.
  =>> E. =>> F. demo.
  =>> E ? F. demo.
  =>> x E. =>>. demo.
Qed.

Lemma demo_arrow_3 :
  forall (a:nat), a = 0%nat -> Sym a.
Proof using.
  dup 5.   =>>. demo.
  =>> E. demo.
  =>> E; =>> F. demo.
  =>> E; =>> F G. demo.
  try (=>> E; =>> F G H). demo.
Qed.

Lemma demo_arrow_4 :
  TestSym.
Proof using.
  dup 2.   =>>. demo.
  =>> E. demo.
Qed.

Lemma demo_arrow_5 :
  forall a:nat, a = 0%nat -> ~ Sym a.
Proof using.
  dup 2.   =>> E. demo.
  =>> E F. demo.
Qed.

Lemma demo_arrow_6 :
  AllSame.
Proof using.
  dup 2.
  =>>. =>>. demo.
  =>> ? E. demo.
Qed.

Lemma demo_arrow_7 :
  AllSameAgain.
Proof using.
  dup 2.
  =>>. =>>. demo.
  =>> ? E. demo.
Qed.

End ArrowTest.

Generalization, naming

Lemma demo_gen_and_generalizes :
  forall P Q : nat -> nat -> nat -> Prop,
  forall a b c, P a b c -> Q a a a -> P b b c -> True.
Proof using.
  intros. dup 3.
  gen H. demo.
  gen a. demo.
  gen b c. demo.
Qed.

Inductive ind : nat -> Prop :=
  | ind_0 : ind 0
  | ind_S : forall n, ind n -> ind (S n)
  | ind_SS : forall n, ind n -> ind (S (S n))
  | ind_P : forall (A:Type) (P:A ->Prop) (f:A ->nat) (a:A),
       ind (f a) -> P a -> ind (S (f a)).

Lemma demo_sets_and_set_eq_and_sets_eq : forall n,
  ind (3 + n) -> ind (7 + n) -> ind (7 + n).
Proof using.
  introv M1 M2. dup 9.
  sets a: (3+n). demo.
  sets b: (7+n). demo.
  set_eq a Ha: (7+n). demo.
  sets_eq a Ha: (7+n). demo.
  sets_eq a: (7+n). demo.
  sets_eq: (7+n). demo.
  set_eq a: (7+n) in M2. demo.
  set_eq a: (7+n) in |-. demo.
  sets_eq <- a: (7+n). demo.
Qed.

Lemma demo_sets_let_and_sets_eq_let : forall n1 n2 : nat,
  (let x := n1 + n2 in x = x ) ->
  (let y := n2 + n1 in let z := y + y in z = z ) ->
  (let t := n1 + n1 in t = t ).
Proof using.
  intros n1 n2 M1 M2. dup 3.
  sets_let a. sets_let b. sets_let c. auto.
  sets_let a in M1. auto.
  sets_eq_let a. sets_eq_let b. sets_eq_let c. auto.
Qed.

Evars

Lemma demo_check_noevar_goal : forall (n:nat),
  (forall m, m = n -> True ) -> True.
Proof using.
  intros. check_noevar_goal. eapply H.
  try check_noevar_goal. dup.
  reflexivity. check_noevar_goal. auto.
Qed.

Unfolding

Definition Id A (x:A) := x.

Lemma demo_unfolds_folds :
  forall a b, a = Id(b) -> Dup a = 0 -> Dup b = Id(0+0).
Proof using.
  intros. dup 2.
  unfolds Dup. demo.
  unfolds Id,Dup.
  subst b.
  folds (Dup a). demo.
Qed.

Definition Twice (P:Prop) := True -> P /\ P.

Lemma demo_unfolds_head_definition :
  forall P:Prop, (True -> P ) -> Twice P -> Twice P.
Proof using.
  introv A B.
  unfolds.
  unfolds in B.
  demo.
Qed.

Simplification

Lemma demo_simpls_and_unsimpl :
  forall a b, Dup a = (1+1) -> Dup b = Id(0+0).
Proof using.
  intros.
  simpls.
  unsimpl (0+0).
  unsimpl (2+0) in H.
  demo.
Qed.

Substitution

Lemma subst_hyp_demo : forall (x y x' y' z z' : nat) (P:nat ->Prop),
  (x ,y ,z ) = (x',y',z') ->
  P x -> P x' -> P y -> P y' -> P z -> P z' ->
  z = z'.
Proof using.
  introv H. intros.
  subst_hyp_base H. auto.
Qed.

Rewriting

Lemma demo_rewrites :
  (forall n m, m + n = n + m ) -> 3 + 4 = 7.
Proof using.
  introv H. dup.
  rewrites (rm H). demo.
  rewrites (>> H __ 3). demo.
Qed.

Lemma demo_rewrites_at : forall x y z,
  x = y + y -> x + x = z -> z + z = x + x + x + x.
Proof using.
  introv E H. dup.
  rewrite E. demo.
  rewrites E at 2.
  rewrites E at 2 in H.
  rewrites <- H at 2.
  demo.
Qed.

Lemma demo_rewrite_all :
  (forall n, n + 0 = 0 + n ) ->
  (3 + 0) + 0 = 5 + 0.
Proof using.
  intros E.
  rewrite_all E. demo.
Qed.

Lemma demo_asserts_and_cuts_rewrite : forall n,
  0 < n < 2 -> P1 1 -> P1 n.
Proof using.
  introv Lt H. dup 2.
  asserts_rewrite (n = 1). demo. demo.
  cuts_rewrite (n = 1). demo. demo.
Qed.

Lemma demo_replaces : forall a b, a = b + b -> a + a + a = 3 * a.
Proof using.
  intros. dup 3.
  replaces a with 3. demo. demo.
  replaces a at 2 with 5. demo. demo.
  replaces b at 2 with 4 in H. demo. demo.
Qed.

Lemma demo_pi_rewrite : forall (P:Prop) (X:P ->nat) (p1 p2:P),
   X p1 + X p2 = X p2 + X p1.
Proof using.
  intros. pi_rewrite p1. reflexivity.
Qed.

Inversions

Inductive even_shift : nat -> nat -> Prop :=
  | even_0 : even_shift 0 2
  | even_SS : forall n m, even_shift n m ->
              even_shift (S (S n)) (S (S m)).

Lemma demo_invert :
  even_shift 4 8 -> False.
Proof using.
  intros P. dup 12.
  inversion P. inversion H7. inversion H10.
  inversions P. inversions H7. inversions H8.
  invert P. introv P' EQ1 EQ2. demo.
  invert P as P' EQ1 EQ2. demo.
  inverts P. inverts H7. inverts H8.
  inverts P as P'. inverts P' as P''. inverts P''.
  inverts P as P. inverts P as P. inverts P.
  inverts P as. introv P'. demo.
  invert keep P. intros. demo.
  inverts keep P as P' EQ1 EQ2. demo.
  inverts keep P as. introv P'. demo.
  lets_inverts (conj P P) as H1 H2. demo.
Qed.

Inductive Behave : Type :=
  | Behave_intro :
      forall (A:Type) (F:A ->nat) (P:A ->Prop), Behave.

Inductive behave : nat -> Behave -> Prop :=
  | behave_intro : forall (A:Type) (F:A ->nat) (P:A ->Prop) V,
      P V -> behave (F V) (@Behave_intro A F P).

Lemma demo_dependent_invert :
  behave 4 (Behave_intro (fun x:nat => x) (fun x:nat => x <> 3))
  -> False.
Proof using.
  intros H. dup 3.
  inversion H. demo.
  inverts H. demo.
  inverts H as R1 R2 R3. demo.
Qed.

Lemma demo_inject_and_injects : forall a b c,
  (a ,b ,c ) = (1,2,3) -> b = 2.
Proof using.
  introv EQ. dup 5.
  injection EQ. demo.
  inject EQ. demo.
  inject EQ as EQ1 EQ2 EQ3. demo.
  injects EQ. demo.
  symmetry in EQ. injects EQ. demo.
Qed.

Case_if

Lemma demo_case_if : forall b c :bool,
  (if b then true else true ) = false ->
  (if c then true else true ) = true.
Proof using.
  intros. dup 4.
  case_if. auto. auto.
  case_if as P. auto. auto.
  case_if in H.
  case_if in H as P.
Qed.

F_equal

Lemma demo_fequals_1 : forall a b c d,
  b = d -> d = 2 -> a = 1 ->
  (a ,b ,c ) = (1,2,3).
Proof using.
  intros. dup 3.
  f_equal. f_equal. demo. demo. demo.
  fequal. demo. demo. demo.
  fequals. demo.
Qed.

Lemma demo_fequals_2 : forall f a b c d,
  b = d -> d = 2 -> a = 1 ->
  f a b c = f 1 2 3 :> nat.
Proof using.
  intros. dup 2.
  fequal. demo. demo. demo.
  fequals. demo.
Qed.

fequals supports proof irrelevance

Lemma demo_fequal_post :
forall (P:Prop) (X:P ->nat) (p1 p2:P), X p1 = X p2.
Proof using. intros. fequals. Qed.

Induction

Inductive natequal : nat -> nat -> Prop :=
| natequal_O : natequal 0 0
| natequal_S : forall n, natequal n n -> natequal (S n) (S n).

N-ary splitting and branching

Definition test_split_1 := H1 /\ H2 /\ H3.
Definition test_split_2 := H4 /\ H5 /\ H6 /\ test_split_1.
Definition test_split_3 := test_split_2.

Lemma demo_splits : test_split_3.
Proof using.
  dup 4.
  split. demo. split. demo. split. demo. split. demo. demo.
  splits 4. demo. demo. demo. demo.
  splits 3. demo. demo. demo.
  splits. demo. demo. demo. splits. demo. demo. demo.
Qed.

Lemma demo_branch :
  1 = 2 \/ 2 = 3 \/ 3 = 4 \/ 4 = 4 \/ 4 = 5 \/ 5 = 6.
Proof using.
  dup 6.
  branch 1 of 6. demo.
  branch 4 of 6. auto.
  branch 6 of 6. demo.
  branch 1. demo.
  branch 4. auto.
  branch 6. demo.
Qed.

Lemma demo_destructs :
  1 = 2 /\ (2 = 3 /\ 3 = 4) /\ 4 = 5 -> True.
Proof using.
  intros H. destructs H. demo.
Qed.

Hide, clears, sorts

Parameter lemma_hide : forall n, n + 0 = n.

Lemma demo_hide_hyps : forall x:nat, x + 0 = x.
Proof using.
  intros.
  generalize (lemma_hide : Something). intros H.
  generalize (lemma_hide : Something). intros H'.
  show_hyp H.
  hide_hyp H.
  show_hyps.
  hide_hyps.
  hnf in H.
  apply H'.
Qed.

Lemma demo_hide_def : forall x:nat,
   let y := x + x in let z := y in y + 0 = y.
Proof using.
  intros.
  hide_def y.
  hide_def z.
  show_def y.
  show_def z.
  hide_defs.
  show_defs.
  hide_def y.
  unfold y.
  show_def.
  demo.
Qed.

Lemma demo_hide_generic : forall x:nat,
   let y := x + x + x + x in let z := y in y + 0 = y.
Proof using.
demo.
Qed.

Lemma demo_hide_term : forall x,
  x + x + x = 3.
Proof using.
  intros.
  hide_term (x+x+x).
  show_term.
  match goal with |- ?T = _ => hide_term T end.
  demo.
Qed.

Lemma demo_clears : forall (x y z : nat) (A B : Prop),
  (x > 0) ->
  (x <> y ) ->
  (A <-> B ) ->
  True.
Proof using.
  introv z Pos Neq Iff. dup 5.
  clears y. demo.
  clears x. demo.
  clears x y. demo.
  clears Neq A. demo.
  clears. demo.
Qed.

Lemma demo_sort :
  forall n : nat,
  n > 0 ->
  forall P Q : Prop,
  (P <-> Q ) ->
  forall m : nat,
  m <> n ->
  forall K : nat -> Prop,
  K n ->
  forall p,
  K (m +p) ->
  True.
Proof using.
  intros.
  sort. demo.
Qed.

Admit

Lemma demo_admit : forall n m p : nat,
  n > m -> m >= p -> n > p.
Proof using.
  intros. dup 6.
  admits R1: (m = m). demo.
  admits (R1&R2): (m = m /\ n > m+1). demo.
  admits (q&Q): (exists q, q > p). demo.
  admits: (m <> n). demo.
  admit_rewrite (m = n) in H0. demo.
  dup.
    induction p. demo. demo.
    admit_goal IH. destruct p. demo. demo.
Qed.

Advanced instantiation

Lemma demo_lets_of : forall (x y : nat) (A B : Prop),
  (x > 0) ->
  (x <> y ) ->
  (A <-> B ) ->
  (forall n, n > 0 -> forall m, n <> m -> exists k, k <> m ) ->
  (forall n : nat,
   n > 0 ->
   forall P Q : Prop,
   (P <-> Q ) ->
   forall m : nat,
   n <> m ->
   forall K : nat -> Prop,
   K n ->
   forall p,
   K (m +p) ->
   True ) ->
  True.
Proof using.
  introv Pos Neq Iff L M.

  lets P: M Iff. eauto. clear P.
  lets P: (>> M Neq). eauto. eauto. clear P.
  lets P: (>> M __ y). eauto. eauto. clear P.
  lets P: (>> M x __ B). eauto. instantiate (1:=A) in P. clear P.
  lets P: (>> M __ y Neq). eauto. eauto. clear P.
  lets P: M Pos A B Neq. eauto. clear P.
  lets k K: (>> L Pos ___). eauto. clears k.
  lets k K: (>> L ___). eauto. eauto. clears k.
  forwards R: L. eauto. eauto. clear R.
  forwards R: L Pos. eauto. clear R.
  forwards k K: L. eauto. eauto. clears k.
  forwards [k K]: L Pos y. eauto. clears k.
  forwards k K: (>> L x y). eauto. eauto. clears k.
  lets k K: (>> L Neq). eauto. clears k.
  auto.
Qed.

Lemma demo_forwards_1 : forall x : nat, x > 1 ->
  (forall z, z > 1 -> exists y, z < 2 /\ z <> y ) ->
  True.
Proof using.
  introv Le H. dup 4.
  forwards Q: H. eauto. demo.
  forwards [y [R1 R2]]: H. eauto. demo.
  forwards: H. eauto. demo.
  forwards: Le. demo.
Qed.

Lemma demo_forwards_2 :
  (forall x y : nat, x = y -> x <= y ) ->
  forall a b : nat, a <= a.
Proof using.
  intros. dup.     forwards K: (H a). reflexivity. apply K.
    forwards* K: (H a).
Qed.

Lemma demo_applys_specializes : forall (x y : nat) (A B : Prop),
  (x > 0) ->
  (x <> y ) ->
  (A <-> B ) ->
  (forall n : nat,
   n > 0 ->
   forall P Q : Prop,
   (P <-> Q ) ->
   forall m : nat,
   m <> n ->
   True ) ->
  True.
Proof using.
  introv Pos Neq Iff M. dup 17.
  applys (>> M Pos). eauto. eauto.
  applys (>> M A B). eauto. eauto. eauto.
  applys (>> M Pos Iff). eauto.
  applys (>> M Iff). eauto. eauto.
  applys (>> M x Iff). eauto. eauto.
  applys M x Iff. eauto. eauto.
  specializes M (>> 3). auto.
  specializes M (>> 3 A B). auto. auto.
  specializes M (>> A __ __). eauto. eauto. auto.
  specializes M (>> Pos Iff 2). eauto. auto.
  specializes M (>> Pos ___). eauto. eauto. auto.
  specializes M (>> __ B ___). eauto. eauto. eauto. auto.
  specializes M __. specializes M __. eauto. auto.
  specializes M ___. eauto. eauto. eauto. auto.
  applys (>> M (rm Pos) Iff). eauto.
  specializes M (>> (proj1 (conj (rm Pos) Neq))). auto.
Qed.

Similar demos, showing how head definitions are unfolded

Definition mydef := forall (n m : nat), n = m -> False.

Lemma demo_specializes_definition :
forall (i:nat), mydef -> i <> i.
Proof using.
introv H. dup 6.

specializes one by one

specializes H i. specializes H i.
specializes H (refl_equal i). false.

specializes all arguments

specializes H i i (refl_equal i). false.

specializes skipping some arguments

specializes H (refl_equal i). false.

forwards all arguments

forwards: H. apply (refl_equal i). false.

forwards on one arguments

forwards M: H i. reflexivity. false.

build using lets

lets: (>> H (refl_equal i)). false.
Qed.

Unfolding occurs recursively

Definition outerdef := mydef.

Lemma demo_specializes_definition_2 :
forall (i:nat), outerdef -> i <> i.
Proof using.
introv H. dup 6.

specializes one by one

specializes H i. specializes H i.
specializes H (refl_equal i). false.

specializes all arguments

specializes H i i (refl_equal i). false.

specializes skipping some arguments

specializes H (refl_equal i). false.

forwards all arguments

forwards: H. apply (refl_equal i). false.

forwards on one arguments

forwards M: H i. reflexivity. false.

build using lets

lets: (>> H (refl_equal i)). false.
Qed.

On the other hand, definitions that are not at head position are not unfolded

Definition nesteddef := forall (n:nat), mydef.

Lemma demo_specializes_definition_3 :
forall (i:nat), nesteddef -> outerdef.
Proof using.
intros i H. dup 4.

forwards does not instantiate mydef from H

forwards K: H i. demo.

... unless explicitely visible

unfold nesteddef, mydef in H.
forwards K: H i. apply (refl_equal i). false.

yet, it should be possible to instantiate arguments inside mydef if providing explicit arguments

lets K: (>> H i i). demo.
lets K: (>> H i (refl_equal i)). demo.
Qed.

Introduction of equalities to enable apply to work

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 using.
  introv H E L. dup 4.
  try apply H.
  eapply equates_2. apply H. auto.
  eapply equates_2; eauto.
  equates 2. demo. demo.
Admitted.
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.
Admitted.
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.
Admitted.

Induction on height of a derivation

Section IndHeight.

Lambda calculus

Inductive trm : Type :=
  | trm_var : nat -> trm
  | trm_abs : nat -> trm -> trm
  | trm_app : trm -> trm -> trm.

Parameter subst : nat -> trm -> trm -> trm.

Original big-step reduction judgment

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.

Same judgment, with an index to bound the height

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) => omega.

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; omega | autos* ]).
Qed.

Lemma bigredh_bigred : forall n t v,
  bigredh n t v -> bigred t v.
Proof using. introv H. induction* H. Qed.

Lemma bigred_bigredh : forall t v,
  bigred t v -> exists n, bigredh n t v.
Proof using. hint bigredh_lt. introv H. induction H; try induct_height. Qed.

After exploiting this last lemma, it is possible to perform an induction on the height of a derivation by doing induction n.

End IndHeight.

Notation for exists

Lemma demo_exist :
  exists x1 x2 x3, x1 = x2 /\ x2 = x3 /\ x3 = 0.
Proof using.
  dup 7.
  exists 0 0 0. auto.
  exists~ 0 0 0.
  exists __ 0 __. demo.
  exists 0 ___.
  exists___ 3. demo.
  exists___. demo.
Admitted.

'let-binding

Definition let_binding_test_1 :
  ('let x := 3 in 'let y := x + x in y + y ) = 12.
Proof using.
  dup 3.
  reflexivity.
  simpl.   let_simpl.
  let_simpl.
  reflexivity.
  let_name.   let_name as z.
  subst x. subst z. reflexivity.
Qed.

Definition let_binding_test_2 :
  ('let x := 3 in 'let y := x + x in y + y ) = 12 -> True.
Proof using.
  dup 2; intros H.
  simpl in H.   let_simpl in H.
  let_simpl in H.
  auto.
  let_name in H.
  let_name in H as z.
  subst x. subst z. auto.
Qed.