Week 3: Introduction to proof scripting and Ltac

Author: Adam Chlipala, with modifications by CS-428 staff.
License: No redistribution allowed (usage by permission in CS-428).

Ltac Programming Basics

We have already seen a few examples of Ltac programs, without much explanation. Ltac is the proof-scripting language built into Coq. Actually, every primitive step in our proofs has been a (degenerate, small) Ltac program. Let's take a bottom-up look at more Ltac features.

We've seen match goal tactics a few times so far. They allow syntactic inspection of hypothesis and conclusion formulas of current goals, where we pick tactics to run based on what we find. Here's a simple example to find an if and do a case split based on its test expression.

Ltac find_if :=
  match goal with
    | [ |- if ?X then _ else _ ] => destruct X
  end.

Here's a proof that becomes trivial, given find_if. You can imagine a whole family of similar theorems that also become trivial.

Theorem hmm : forall (a b c : bool),
  if a
    then if b
      then True
      else True
    else if c
      then True
      else True.forall a b c : bool,
if a
then if b then True else True
else if c then True else True
Proof.forall a b c : bool,
if a
then if b then True else True
else if c then True else True
  intros.a, b, c: bool
if a
then if b then True else True
else if c then True else True
  repeat find_if.c: bool
True
c: bool
True
b: bool
True
b: bool
True (* Note `repeat` for "run over and over
                     until you can't progress." *)
  trivial.c: bool
True
b: bool
True
b: bool
True (* A fun tactic that consults a database of
              really boring steps. *)
  trivial.b: bool
True
b: bool
True
  trivial.b: bool
True
  trivial.

Let's write that again with more automation.

  Restart.forall a b c : bool,
if a
then if b then True else True
else if c then True else True
  intros; repeat find_if; trivial.
Qed.

Another very useful Ltac building block is context patterns.

Ltac find_if_inside :=
  match goal with
    | [ |- context[if ?X then _ else _] ] => destruct X
  end.

The behavior of this tactic is to find any subterm of the conclusion that is an if and then destruct the test expression. This version subsumes find_if. The general behavior of context (an Ltac keyword) is to allow matching in arbitrary subterms.

Theorem hmm' : forall (a b c : bool),
  if a
    then if b
      then True
      else True
    else if c
      then True
      else True.forall a b c : bool,
if a
then if b then True else True
else if c then True else True
Proof.forall a b c : bool,
if a
then if b then True else True
else if c then True else True
  intros; repeat find_if_inside; trivial.
Qed.

We can also use find_if_inside to prove goals that find_if does not simplify sufficiently.

Theorem hmm2 : forall (a b : bool),
  (if a then 42 else 42) = (if b then 42 else 42).forall a b : bool,
(if a then 42 else 42) = (if b then 42 else 42)
Proof.forall a b : bool,
(if a then 42 else 42) = (if b then 42 else 42)
  intros; repeat find_if_inside; reflexivity.
Qed.

Implementing a custom `tauto`

In class, we develop our own implementation of propositional one feature at a time, but here's just the final product. To understand it, we print the definitions of the logical connectives. Interestingly enough, they are special cases of the machinery we met previously for inductive relations!

Print True.Inductive True : Prop :=  I : True.
Print False.Inductive False : Prop :=  .
Locate "/\".Notation "A /\ B" := (and A B) : type_scope
  (default interpretation)
Print and.Inductive and (A B : Prop) : Prop :=
    conj : A -> B -> A /\ B.

Arguments and (A B)%type_scope
Arguments conj [A B]%type_scope _ _
Locate "\/".Notation "A \/ B" := (or A B) : type_scope
  (default interpretation)
Print or.Inductive or (A B : Prop) : Prop :=
    or_introl : A -> A \/ B | or_intror : B -> A \/ B.

Arguments or (A B)%type_scope
Arguments or_introl [A B]%type_scope _, [_] _ _
Arguments or_intror [A B]%type_scope _, _ [_] _

(Implication (->) is built into Coq, so nothing to look up there.)

Ltac my_tauto :=
  repeat match goal with
	   | [ H : ?P |- ?P ] => exact H

	   | [ |- True ] => constructor
	   | [ |- _ /\ _ ] => constructor
	   | [ |- _ -> _ ] => intro

	   | [ H : False |- _ ] => destruct H
	   | [ H : _ /\ _ |- _ ] => destruct H
	   | [ H : _ \/ _ |- _ ] => destruct H

	   | [ H1 : ?P -> ?Q, H2 : ?P |- _ ] => specialize (H1 H2)
	 end.

Section propositional.
  Variables P Q R : Prop.

  Theorem propositional : (P \/ Q \/ False) /\ (P -> Q) -> True /\ Q.P, Q, R: Prop
(P \/ Q \/ False) /\ (P -> Q) -> True /\ Q
  Proof.P, Q, R: Prop
(P \/ Q \/ False) /\ (P -> Q) -> True /\ Q
    my_tauto.
  Qed.
End propositional.

Backtracking

match goal has useful backtracking semantics. When one rule fails, we backtrack automatically to the next one.

For instance, this (unnecessarily verbose) proof script works:

Theorem m1 : True.True
Proof.True
  match goal with
    | [ |- _ ] => intro
    | [ |- True ] => constructor
  end.
Qed.

The example shows how failure can move to a different pattern within a match. Failure can also trigger an attempt to find a different way of matching a single pattern. Consider another example:

Theorem m2 : forall P Q R : Prop, P -> Q -> R -> Q.forall P Q R : Prop, P -> Q -> R -> Q
Proof.forall P Q R : Prop, P -> Q -> R -> Q
  intros; match goal with
            | [ H : _ |- _ ] => idtac H
          end.H1
P, Q, R: Prop
H: P
H0: Q
H1: R
Q

Coq prints "H1". By applying idtac with an argument, a convenient debugging tool for "leaking information out of matches," we see that this match first tries binding H to H1, which cannot be used to prove Q. Nonetheless, the following variation on the tactic succeeds at proving the goal:

  match goal with
    | [ H : _ |- _ ] => idtac H; exact H
  end.H1
H0
Qed.

The tactic first unifies H with H1, as before, but exact H fails in that case, so the tactic engine searches for more possible values of H. Eventually, it arrives at the correct value, so that exact H and the overall tactic succeed.

Instantiating quantifiers

Let's try some more ambitious reasoning, with quantifiers. We'll be instantiating quantified facts heuristically. If we're not careful, we get in a loop repeating the same instantiation forever. We'll need a way to check that a fact is not already known. Here's a tactic:

Ltac notHyp P :=
  match goal with
  | [ _ : P |- _ ] =>
      fail 1 (* A hypothesis already asserts this fact. *)
  | _ =>
      match P with
      | ?P1 /\ ?P2 =>
          (* Check each conjunct of `P` separately, since they might
             be known by different means. *)
          first [ notHyp P1 | notHyp P2 | fail 2 ]
      | _ =>
          idtac (* If we manage to get this far, then we found no
                   redundancy, so declare success. *)
      end
  end.

The number for fail N indicates failing at the backtracking point N levels out from where we are. first applies the first tactic that does not fail.

This tactic adds a fact to the context, only if it is not already present.

Ltac extend pf :=
  let t := type of pf in
    notHyp t; pose proof pf.

With these tactics defined, we can write a tactic completer for, among other things, adding to the context all consequences of a set of simple first-order formulas.

Ltac completer :=
  repeat match goal with
    | [ H : _ /\ _ |- _ ] => destruct H
    | [ H : ?P -> ?Q, H' : ?P |- _ ] => specialize (H H')

    | [ H : forall x, ?P x -> _, H' : ?P ?X |- _ ] => extend (H X H')

    | [ |- _ /\ _ ] => constructor
    | [ |- forall x, _ ] => intro
    | [ |- _ -> _ ] => intro (* Note: Redundant with rule above *)
    end.

Section firstorder.
  Variable A : Set.
  Variables P Q R S : A -> Prop.

  Hypothesis H1 : forall x, P x -> Q x /\ R x.
  Hypothesis H2 : forall x, R x -> S x.

  Theorem fo : forall (y x : A), P x -> S x.A: Set
P, Q, R, S: A -> Prop
H1: forall x : A, P x -> Q x /\ R x
H2: forall x : A, R x -> S x
A -> forall x : A, P x -> S x
  Proof.A: Set
P, Q, R, S: A -> Prop
H1: forall x : A, P x -> Q x /\ R x
H2: forall x : A, R x -> S x
A -> forall x : A, P x -> S x
    completer.A: Set
P, Q, R, S: A -> Prop
H1: forall x : A, P x -> Q x /\ R x
H2: forall x : A, R x -> S x
y, x: A
H: P x
H0: Q x
H3: R x
H4: S x
S x
    assumption.
  Qed.
End firstorder.

Functional Programming in Ltac

Let's write a list-length function in Ltac rather than Gallina. In class, we'll muddle through some intermediate versions before getting to the first version that at least parses.

Module Import FirstTry.
  Ltac length ls :=
    match ls with
    | nil => O
    | _ :: ?ls' => constr:(S (length ls'))
    end.
End FirstTry.

Goal False.False
  let n := length (1 :: 2 :: 3 :: nil) in
    pose n.n:= S (length [2; 3]): nat
False
Abort.

Something went wrong there.

Ltac length ls :=
  match ls with
    | nil => O
    | _ :: ?ls' =>
      let ls'' := length ls' in
        constr:(S ls'')
  end.

Goal False.False
  let n := length (1 :: 2 :: 3 :: nil) in
    pose n.n:= 3: nat
False
Abort.

Here's a map implementation in Ltac. Strangely, it needs to be passed the type of the new list explicitly.

Ltac map T f :=
  let rec map' ls :=
    match ls with
      | nil => constr:(@nil T)
      | ?x :: ?ls' =>
        let x' := f x in
          let ls'' := map' ls' in
            constr:(x' :: ls'')
    end in
  map'.

Goal False.False
  let ls := map (nat * nat)%type
               ltac:(fun x => constr:((x, x))) (1 :: 2 :: 3 :: nil) in
    pose ls.l:= [(1, 1); (2, 2); (3, 3)]: list (nat * nat)
False
Abort.

Now let's revisit length and see how we might implement "printf debugging" for it.

Module Import WithPrinting.
  Ltac length ls :=
    idtac ls;
    match ls with
    | nil => O
    | _ :: ?ls' =>
      let ls'' := length ls' in
      constr:(S ls'')
    end.
End WithPrinting.

Goal False.False
  let n := length (1 :: 2 :: 3 :: nil) in
       pose n.variable n should be bound to a term.

Oh, that has a dynamic type error.

Abort.

The problem is that Ltac as a language contains several datatypes. One of them is "tactic sequence," which can't be mixed with other datatypes like "term in the logic." Tactic sequences don't return results. We can use continuation-passing style as a mitigation.

Module Import WithPrintingFixed.
  Ltac length ls k :=
    idtac ls;
    match ls with
    | nil => k O
    | _ :: ?ls' => length ls' ltac:(fun n => k (S n))
    end.
End WithPrintingFixed.

Goal False.False
  length (1 :: 2 :: 3 :: nil) ltac:(fun n => pose n).[1; 2; 3]
[2; 3]
[3]
[]
Abort.

However, it's not always convenient to use continuation-passing style everywhere, so cool kids use the following hack to sneak side effects into otherwise-functional Ltac code.

Module Import WithPrintingFixedWithoutContinuations.
  Ltac length ls :=
    let __ := match constr:(Set) with
              | _ => (* put all your side effects here:*)
                     idtac ls
              end in
    match ls with
    | nil => constr:(O)
    | _ :: ?ls' => let L := length ls' in constr:(S L)
    end.
End WithPrintingFixedWithoutContinuations.

Goal False.False
  let n := length (1 :: 2 :: 3 :: nil) in
  pose n.[1; 2; 3]
[2; 3]
[3]
[]
Abort.

Recursive Proof Search

Let's work on a tactic to try all possible instantiations of quantified hypotheses, attempting to find out where the goal becomes obvious.

Ltac inster n :=
  intuition; (* <-- A fancier version of `tauto` whose details we won't
              *     dwell on *)
    match n with
      | S ?n' =>
        match goal with
        | [ H : forall x : ?T, _, y : ?T |- _ ] =>
            pose proof (H y); inster n'
        end
    end.

Important: when one recursive call fails (happens when n reaches zero and intuition leaves some open goals), the backtracking semantics of match goal cause us to try the next instantiation!

Section test_inster.
  Variable A : Set.
  Variables P Q : A -> Prop.
  Variable f : A -> A.
  Variable g : A -> A -> A.

  Hypothesis H1 : forall x y, P (g x y) -> Q (f x).

  Theorem test_inster : forall x, P (g x x) -> Q (f x).A: Set
P, Q: A -> Prop
f: A -> A
g: A -> A -> A
H1: forall x y : A, P (g x y) -> Q (f x)
forall x : A, P (g x x) -> Q (f x)
  Proof.A: Set
P, Q: A -> Prop
f: A -> A
g: A -> A -> A
H1: forall x y : A, P (g x y) -> Q (f x)
forall x : A, P (g x x) -> Q (f x)
    inster 2.
  Qed.

  Hypothesis H3 : forall u v, P u /\ P v /\ u <> v -> P (g u v).
  Hypothesis H4 : forall u, Q (f u) -> P u /\ P (f u).

  Theorem test_inster2 : forall x y,
      x <> y -> P x -> Q (f y) -> Q (f x).A: Set
P, Q: A -> Prop
f: A -> A
g: A -> A -> A
H1: forall x y : A, P (g x y) -> Q (f x)
H3: forall u v : A, P u /\ P v /\ u <> v -> P (g u v)
H4: forall u : A, Q (f u) -> P u /\ P (f u)
forall x y : A, x <> y -> P x -> Q (f y) -> Q (f x)
  Proof.A: Set
P, Q: A -> Prop
f: A -> A
g: A -> A -> A
H1: forall x y : A, P (g x y) -> Q (f x)
H3: forall u v : A, P u /\ P v /\ u <> v -> P (g u v)
H4: forall u : A, Q (f u) -> P u /\ P (f u)
forall x y : A, x <> y -> P x -> Q (f y) -> Q (f x)
    inster 3.
  Qed.
End test_inster.

A fancier example of proof search (probably skipped on first reading/run-through)

Definition imp (P1 P2 : Prop) := P1 -> P2.
Infix "-->" := imp (no associativity, at level 95).
Ltac imp := unfold imp; firstorder.

These lemmas about imp will be useful in the tactic that we will write.

Theorem and_True_prem : forall P Q,
  (P /\ True --> Q)
  -> (P --> Q).forall P Q : Prop, P /\ True --> Q -> P --> Q
Proof.forall P Q : Prop, P /\ True --> Q -> P --> Q
  imp.
Qed.

Theorem and_True_conc : forall P Q,
  (P --> Q /\ True)
  -> (P --> Q).forall P Q : Prop, P --> Q /\ True -> P --> Q
Proof.forall P Q : Prop, P --> Q /\ True -> P --> Q
  imp.
Qed.

Theorem pick_prem1 : forall P Q R S,
  (P /\ (Q /\ R) --> S)
  -> ((P /\ Q) /\ R --> S).forall P Q R S : Prop,
P /\ Q /\ R --> S -> (P /\ Q) /\ R --> S
Proof.forall P Q R S : Prop,
P /\ Q /\ R --> S -> (P /\ Q) /\ R --> S
  imp.
Qed.

Theorem pick_prem2 : forall P Q R S,
  (Q /\ (P /\ R) --> S)
  -> ((P /\ Q) /\ R --> S).forall P Q R S : Prop,
Q /\ P /\ R --> S -> (P /\ Q) /\ R --> S
Proof.forall P Q R S : Prop,
Q /\ P /\ R --> S -> (P /\ Q) /\ R --> S
  imp.
Qed.

Theorem comm_prem : forall P Q R,
  (P /\ Q --> R)
  -> (Q /\ P --> R).forall P Q R : Prop, P /\ Q --> R -> Q /\ P --> R
Proof.forall P Q R : Prop, P /\ Q --> R -> Q /\ P --> R
  imp.
Qed.

Theorem pick_conc1 : forall P Q R S,
  (S --> P /\ (Q /\ R))
  -> (S --> (P /\ Q) /\ R).forall P Q R S : Prop,
S --> P /\ Q /\ R -> S --> (P /\ Q) /\ R
Proof.forall P Q R S : Prop,
S --> P /\ Q /\ R -> S --> (P /\ Q) /\ R
  imp.
Qed.

Theorem pick_conc2 : forall P Q R S,
  (S --> Q /\ (P /\ R))
  -> (S --> (P /\ Q) /\ R).forall P Q R S : Prop,
S --> Q /\ P /\ R -> S --> (P /\ Q) /\ R
Proof.forall P Q R S : Prop,
S --> Q /\ P /\ R -> S --> (P /\ Q) /\ R
  imp.
Qed.

Theorem comm_conc : forall P Q R,
  (R --> P /\ Q)
  -> (R --> Q /\ P).forall P Q R : Prop, R --> P /\ Q -> R --> Q /\ P
Proof.forall P Q R : Prop, R --> P /\ Q -> R --> Q /\ P
  imp.
Qed.

Ltac search_prem tac :=
  let rec search P :=
    tac
    || (apply and_True_prem; tac)
    || match P with
         | ?P1 /\ ?P2 =>
           (apply pick_prem1; search P1)
           || (apply pick_prem2; search P2)
       end
  in match goal with
       | [ |- ?P /\ _ --> _ ] => search P
       | [ |- _ /\ ?P --> _ ] => apply comm_prem; search P
       | [ |- _ --> _ ] => progress (tac || (apply and_True_prem; tac))
     end.

Ltac search_conc tac :=
  let rec search P :=
    tac
    || (apply and_True_conc; tac)
    || match P with
         | ?P1 /\ ?P2 =>
           (apply pick_conc1; search P1)
           || (apply pick_conc2; search P2)
       end
  in match goal with
       | [ |- _ --> ?P /\ _ ] => search P
       | [ |- _ --> _ /\ ?P ] => apply comm_conc; search P
       | [ |- _ --> _ ] => progress (tac || (apply and_True_conc; tac))
     end.

Theorem False_prem : forall P Q,
  False /\ P --> Q.forall P Q : Prop, False /\ P --> Q
Proof.forall P Q : Prop, False /\ P --> Q
  imp.
Qed.

Theorem True_conc : forall P Q : Prop,
  (P --> Q)
  -> (P --> True /\ Q).forall P Q : Prop, P --> Q -> P --> True /\ Q
Proof.forall P Q : Prop, P --> Q -> P --> True /\ Q
  imp.
Qed.

Theorem Match : forall P Q R : Prop,
  (Q --> R)
  -> (P /\ Q --> P /\ R).forall P Q R : Prop, Q --> R -> P /\ Q --> P /\ R
Proof.forall P Q R : Prop, Q --> R -> P /\ Q --> P /\ R
  imp.
Qed.

Theorem ex_prem : forall (T : Type) (P : T -> Prop) (Q R : Prop),
  (forall x, P x /\ Q --> R)
  -> (ex P /\ Q --> R).forall (T : Type) (P : T -> Prop) (Q R : Prop),
(forall x : T, P x /\ Q --> R) ->
(exists y, P y) /\ Q --> R
Proof.forall (T : Type) (P : T -> Prop) (Q R : Prop),
(forall x : T, P x /\ Q --> R) ->
(exists y, P y) /\ Q --> R
  imp.
Qed.

Theorem ex_conc : forall (T : Type) (P : T -> Prop) (Q R : Prop) x,
  (Q --> P x /\ R)
  -> (Q --> ex P /\ R).forall (T : Type) (P : T -> Prop) (Q R : Prop) (x : T),
Q --> P x /\ R -> Q --> (exists y, P y) /\ R
Proof.forall (T : Type) (P : T -> Prop) (Q R : Prop) (x : T),
Q --> P x /\ R -> Q --> (exists y, P y) /\ R
  imp.
Qed.

Theorem imp_True : forall P,
  P --> True.forall P : Prop, P --> True
Proof.forall P : Prop, P --> True
  imp.
Qed.

Ltac matcher :=
  intros;
  repeat search_prem
         ltac:(simple apply False_prem ||
                 (simple apply ex_prem; intro));
  repeat search_conc
         ltac:(simple apply True_conc ||
                 simple eapply ex_conc ||
                   search_prem ltac:(simple apply Match));
      try simple apply imp_True.

Our tactic succeeds at proving a simple example.

Theorem t2 : forall P Q : Prop,
  Q /\ (P /\ False) /\ P --> P /\ Q.forall P Q : Prop, Q /\ (P /\ False) /\ P --> P /\ Q
Proof.forall P Q : Prop, Q /\ (P /\ False) /\ P --> P /\ Q
  matcher.
Qed.

In the generated proof, we find a trace of the workings of the search tactics.

Print t2.t2 =
fun P Q : Prop =>
comm_prem ((P /\ False) /\ P) Q (P /\ Q)
  (pick_prem1 (P /\ False) P Q (P /\ Q)
     (pick_prem2 P False (P /\ Q) (P /\ Q)
        (False_prem (P /\ P /\ Q) (P /\ Q))))
     : forall P Q : Prop,
       Q /\ (P /\ False) /\ P --> P /\ Q

Arguments t2 (P Q)%type_scope _

We can also see that matcher is well-suited for destruct where some human intervention is needed after the automation finishes.

Theorem t3 : forall P Q R : Prop,
  P /\ Q --> Q /\ R /\ P.forall P Q R : Prop, P /\ Q --> Q /\ R /\ P
Proof.forall P Q R : Prop, P /\ Q --> Q /\ R /\ P
  matcher.P, Q, R: Prop
True --> R
Abort.

The matcher tactic even succeeds at guessing quantifier instantiations. It is the unification that occurs in uses of the Match lemma that does the real work here.

Theorem t4 : forall (P : nat -> Prop) Q,
    (exists x, P x /\ Q) --> Q /\ (exists x, P x).forall (P : nat -> Prop) (Q : Prop),
(exists x : nat, P x /\ Q) -->
Q /\ (exists x : nat, P x)
Proof.forall (P : nat -> Prop) (Q : Prop),
(exists x : nat, P x /\ Q) -->
Q /\ (exists x : nat, P x)
  matcher.
Qed.

Print t4.t4 =
fun (P : nat -> Prop) (Q : Prop) =>
and_True_prem (exists x : nat, P x /\ Q)
  (Q /\ (exists x : nat, P x))
  (ex_prem nat (fun x : nat => P x /\ Q) True
     (Q /\ (exists x : nat, P x))
     (fun x : nat =>
      pick_prem2 (P x) Q True
        (Q /\ (exists x0 : nat, P x0))
        (Match Q (P x /\ True) (exists x0 : nat, P x0)
           (and_True_conc (P x /\ True)
              (exists x0 : nat, P x0)
              (ex_conc nat (fun x0 : nat => P x0)
                 (P x /\ True) True x
                 (Match (P x) True True
                    (imp_True True)))))))
     : forall (P : nat -> Prop) (Q : Prop),
       (exists x : nat, P x /\ Q) -->
       Q /\ (exists x : nat, P x)

Arguments t4 P%function_scope Q%type_scope _

Creating Unification Variables

A final useful ingredient in tactic crafting is the ability to allocate new unification variables explicitly. Before we are ready to write a tactic, we can try out its ingredients one at a time.

Theorem t5 : (forall x : nat, S x > x) -> 2 > 1.(forall x : nat, S x > x) -> 2 > 1
Proof.(forall x : nat, S x > x) -> 2 > 1
  intros.H: forall x : nat, S x > x
2 > 1

  evar (y : nat).H: forall x : nat, S x > x
y:= ?y: nat
2 > 1

  let y' := eval unfold y in y in
    clear y; specialize (H y').H: S ?y > ?y
2 > 1

  apply H.
Qed.

Ltac newEvar T k :=
  let x := fresh "x" in
  evar (x : T);
  let x' := eval unfold x in x in
    clear x; k x'.

Ltac insterU H :=
  repeat match type of H with
           | forall x : ?T, _ =>
             newEvar T ltac:(fun y => specialize (H y))
         end.

Theorem t5' : (forall x : nat, S x > x) -> 2 > 1.(forall x : nat, S x > x) -> 2 > 1
Proof.(forall x : nat, S x > x) -> 2 > 1
  intro H.H: forall x : nat, S x > x
2 > 1
  insterU H.H: S ?x > ?x
2 > 1
  apply H.
Qed.

This particular example is somewhat silly, since apply by itself would have solved the goal originally. Separate forward reasoning is more useful on hypotheses that end in existential quantifications. Before we go through an example, it is useful to define a variant of insterU that does not clear the base hypothesis we pass to it.

Ltac insterKeep H :=
  let H' := fresh "H'" in
    pose proof H as H'; insterU H'.

Section t6.
  Variables A B : Type.
  Variable P : A -> B -> Prop.
  Variable f : A -> A -> A.
  Variable g : B -> B -> B.

  Hypothesis H1 : forall v, exists u, P v u.
  Hypothesis H2 : forall v1 u1 v2 u2,
    P v1 u1
    -> P v2 u2
    -> P (f v1 v2) (g u1 u2).

  Theorem t6 : forall v1 v2,
    exists u1, exists u2, P (f v1 v2) (g u1 u2).A, B: Type
P: A -> B -> Prop
f: A -> A -> A
g: B -> B -> B
H1: forall v : A, exists u : B, P v u
H2: forall (v1 : A) (u1 : B) (v2 : A) (u2 : B),
P v1 u1 -> P v2 u2 -> P (f v1 v2) (g u1 u2)
forall v1 v2 : A,
exists u1 u2 : B, P (f v1 v2) (g u1 u2)
  Proof.A, B: Type
P: A -> B -> Prop
f: A -> A -> A
g: B -> B -> B
H1: forall v : A, exists u : B, P v u
H2: forall (v1 : A) (u1 : B) (v2 : A) (u2 : B),
P v1 u1 -> P v2 u2 -> P (f v1 v2) (g u1 u2)
forall v1 v2 : A,
exists u1 u2 : B, P (f v1 v2) (g u1 u2)
    intros.A, B: Type
P: A -> B -> Prop
f: A -> A -> A
g: B -> B -> B
H1: forall v : A, exists u : B, P v u
H2: forall (v1 : A) (u1 : B) (v2 : A) (u2 : B),
P v1 u1 -> P v2 u2 -> P (f v1 v2) (g u1 u2)
v1, v2: A
exists u1 u2 : B, P (f v1 v2) (g u1 u2)

    do 2 insterKeep H1.A, B: Type
P: A -> B -> Prop
f: A -> A -> A
g: B -> B -> B
H1: forall v : A, exists u : B, P v u
H2: forall (v1 : A) (u1 : B) (v2 : A) (u2 : B),
P v1 u1 -> P v2 u2 -> P (f v1 v2) (g u1 u2)
v1, v2: A
H': exists u : B, P ?x u
H'0: exists u : B, P ?x0 u
exists u1 u2 : B, P (f v1 v2) (g u1 u2)

    repeat match goal with
             | [ H : ex _ |- _ ] => destruct H
           end.A, B: Type
P: A -> B -> Prop
f: A -> A -> A
g: B -> B -> B
H1: forall v : A, exists u : B, P v u
H2: forall (v1 : A) (u1 : B) (v2 : A) (u2 : B),
P v1 u1 -> P v2 u2 -> P (f v1 v2) (g u1 u2)
v1, v2: A
x0: B
p: P ?x x0
x: B
H: P ?x0@{H':=ex_intro (fun u : B => P ?x u) x0 p} x
exists u1 u2 : B, P (f v1 v2) (g u1 u2)

    eexists.A, B: Type
P: A -> B -> Prop
f: A -> A -> A
g: B -> B -> B
H1: forall v : A, exists u : B, P v u
H2: forall (v1 : A) (u1 : B) (v2 : A) (u2 : B),
P v1 u1 -> P v2 u2 -> P (f v1 v2) (g u1 u2)
v1, v2: A
x0: B
p: P ?x x0
x: B
H: P ?x0@{H':=ex_intro (fun u : B => P ?x u) x0 p} x
exists u2 : B, P (f v1 v2) (g ?u1 u2)
    eexists.A, B: Type
P: A -> B -> Prop
f: A -> A -> A
g: B -> B -> B
H1: forall v : A, exists u : B, P v u
H2: forall (v1 : A) (u1 : B) (v2 : A) (u2 : B),
P v1 u1 -> P v2 u2 -> P (f v1 v2) (g u1 u2)
v1, v2: A
x0: B
p: P ?x x0
x: B
H: P ?x0@{H':=ex_intro (fun u : B => P ?x u) x0 p} x
P (f v1 v2) (g ?u1 ?u2)
    apply H2.A, B: Type
P: A -> B -> Prop
f: A -> A -> A
g: B -> B -> B
H1: forall v : A, exists u : B, P v u
H2: forall (v1 : A) (u1 : B) (v2 : A) (u2 : B),
P v1 u1 -> P v2 u2 -> P (f v1 v2) (g u1 u2)
v1, v2: A
x0: B
p: P ?x x0
x: B
H: P ?x0@{H':=ex_intro (fun u : B => P ?x u) x0 p} x
P v1 ?u1
A, B: Type
P: A -> B -> Prop
f: A -> A -> A
g: B -> B -> B
H1: forall v : A, exists u : B, P v u
H2: forall (v1 : A) (u1 : B) (v2 : A) (u2 : B),
P v1 u1 -> P v2 u2 -> P (f v1 v2) (g u1 u2)
v1, v2: A
x0: B
p: P ?x x0
x: B
H: P ?x0@{H':=ex_intro (fun u : B => P ?x u) x0 p} x
P v2 ?u2
    exact H.A, B: Type
P: A -> B -> Prop
f: A -> A -> A
g: B -> B -> B
H1: forall v : A, exists u : B, P v u
H2: forall (v1 : A) (u1 : B) (v2 : A) (u2 : B),
P v1 u1 -> P v2 u2 -> P (f v1 v2) (g u1 u2)
v1, v2: A
x0: B
p: P ?x x0
x: B
H: P v1 x
P v2 ?u2
    exact p.

Next week, we'll meet eauto, which can do these last steps automatically.

  Qed.
End t6.

Here's an example where something bad happens.

Section t7.
  Variables A B : Type.
  Variable Q : A -> Prop.
  Variable P : A -> B -> Prop.
  Variable f : A -> A -> A.
  Variable g : B -> B -> B.

  Hypothesis H1 : forall v, Q v -> exists u, P v u.
  Hypothesis H2 : forall v1 u1 v2 u2,
    P v1 u1
    -> P v2 u2
    -> P (f v1 v2) (g u1 u2).

  Theorem t7 : forall v1 v2,
      Q v1 -> Q v2 -> exists u1, exists u2, P (f v1 v2) (g u1 u2).A, B: Type
Q: A -> Prop
P: A -> B -> Prop
f: A -> A -> A
g: B -> B -> B
H1: forall v : A, Q v -> exists u : B, P v u
H2: forall (v1 : A) (u1 : B) (v2 : A) (u2 : B),
P v1 u1 -> P v2 u2 -> P (f v1 v2) (g u1 u2)
forall v1 v2 : A,
Q v1 ->
Q v2 -> exists u1 u2 : B, P (f v1 v2) (g u1 u2)
  Proof.A, B: Type
Q: A -> Prop
P: A -> B -> Prop
f: A -> A -> A
g: B -> B -> B
H1: forall v : A, Q v -> exists u : B, P v u
H2: forall (v1 : A) (u1 : B) (v2 : A) (u2 : B),
P v1 u1 -> P v2 u2 -> P (f v1 v2) (g u1 u2)
forall v1 v2 : A,
Q v1 ->
Q v2 -> exists u1 u2 : B, P (f v1 v2) (g u1 u2)
    intros; do 2 insterKeep H1;
      repeat match goal with
               | [ H : ex _ |- _ ] => destruct H
             end; eauto.

Oh, two trivial goals remain.

    Unshelve.A, B: Type
Q: A -> Prop
P: A -> B -> Prop
f: A -> A -> A
g: B -> B -> B
H1: forall v : A, Q v -> exists u : B, P v u
H2: forall (v1 : A) (u1 : B) (v2 : A) (u2 : B),
P v1 u1 -> P v2 u2 -> P (f v1 v2) (g u1 u2)
v1, v2: A
H: Q v1
H0: Q v2
H': Q v2 -> exists u : B, P v2 u
x0Q v2
A, B: Type
Q: A -> Prop
P: A -> B -> Prop
f: A -> A -> A
g: B -> B -> B
H1: forall v : A, Q v -> exists u : B, P v u
H2: forall (v1 : A) (u1 : B) (v2 : A) (u2 : B),
P v1 u1 -> P v2 u2 -> P (f v1 v2) (g u1 u2)
v1, v2: A
H: Q v1
H0: Q v2
H': exists u : B, P v2 u
H'0: Q v1 -> exists u : B, P v1 u
x2Q v1
    assumption.A, B: Type
Q: A -> Prop
P: A -> B -> Prop
f: A -> A -> A
g: B -> B -> B
H1: forall v : A, Q v -> exists u : B, P v u
H2: forall (v1 : A) (u1 : B) (v2 : A) (u2 : B),
P v1 u1 -> P v2 u2 -> P (f v1 v2) (g u1 u2)
v1, v2: A
H: Q v1
H0: Q v2
H': exists u : B, P v2 u
H'0: Q v1 -> exists u : B, P v1 u
x2Q v1
    assumption.
  Qed.
End t7.

Why did we need to do that extra work? The forall rule was also matching implications!

Module Import FixedInster.
  Ltac insterU tac H :=
    repeat match type of H with
           | forall x : ?T, _ =>
             match type of T with
             | Prop =>
               (let H' := fresh "H'" in
                assert (H' : T) by solve [ tac ];
                specialize (H H'); clear H')
               || fail 1
             | _ =>
               newEvar T ltac:(fun y => specialize (H y))
             end
           end.

  Ltac insterKeep tac H :=
    let H' := fresh "H'" in
      pose proof H as H'; insterU tac H'.
End FixedInster.

Section t7'.
  Variables A B : Type.
  Variable Q : A -> Prop.
  Variable P : A -> B -> Prop.
  Variable f : A -> A -> A.
  Variable g : B -> B -> B.

  Hypothesis H1 : forall v, Q v -> exists u, P v u.
  Hypothesis H2 : forall v1 u1 v2 u2,
    P v1 u1
    -> P v2 u2
    -> P (f v1 v2) (g u1 u2).

  Theorem t7' : forall v1 v2,
      Q v1 -> Q v2 -> exists u1, exists u2, P (f v1 v2) (g u1 u2).A, B: Type
Q: A -> Prop
P: A -> B -> Prop
f: A -> A -> A
g: B -> B -> B
H1: forall v : A, Q v -> exists u : B, P v u
H2: forall (v1 : A) (u1 : B) (v2 : A) (u2 : B),
P v1 u1 -> P v2 u2 -> P (f v1 v2) (g u1 u2)
forall v1 v2 : A,
Q v1 ->
Q v2 -> exists u1 u2 : B, P (f v1 v2) (g u1 u2)
  Proof.A, B: Type
Q: A -> Prop
P: A -> B -> Prop
f: A -> A -> A
g: B -> B -> B
H1: forall v : A, Q v -> exists u : B, P v u
H2: forall (v1 : A) (u1 : B) (v2 : A) (u2 : B),
P v1 u1 -> P v2 u2 -> P (f v1 v2) (g u1 u2)
forall v1 v2 : A,
Q v1 ->
Q v2 -> exists u1 u2 : B, P (f v1 v2) (g u1 u2)
    intros.A, B: Type
Q: A -> Prop
P: A -> B -> Prop
f: A -> A -> A
g: B -> B -> B
H1: forall v : A, Q v -> exists u : B, P v u
H2: forall (v1 : A) (u1 : B) (v2 : A) (u2 : B),
P v1 u1 -> P v2 u2 -> P (f v1 v2) (g u1 u2)
v1, v2: A
H: Q v1
H0: Q v2
exists u1 u2 : B, P (f v1 v2) (g u1 u2)
    do 2 insterKeep ltac:(idtac;
                          match goal with
                          | [ H : Q ?v |- _ ] =>
                              match goal with
                              | [ _ : context[P v _] |- _ ] => fail 1
                              | _ => apply H
                              end
                          end) H1;
    repeat match goal with
           | [ H : ex _ |- _ ] => destruct H
           end; eauto.
  Qed.
End t7'.

One more example of working with existentials:

Theorem t8 : exists p : nat * nat, fst p = 3.exists p : nat * nat, fst p = 3
Proof.exists p : nat * nat, fst p = 3
  econstructor.fst ?p = 3
  instantiate (1 := (3, 2)).fst (3, 2) = 3

We use instantiate to plug in a value for one of the "question-mark variables" in the conclusion. The 1 := part says "first such variable mentioned in the conclusion, counting from right to left."

  reflexivity.
Qed.

A way that plays better with automation:

Theorem t9 : exists p : nat * nat, fst p = 3.exists p : nat * nat, fst p = 3
Proof.exists p : nat * nat, fst p = 3
  econstructor; match goal with
                  | [ |- fst ?x = 3 ] => unify x (3, 2)
                end; reflexivity.
Qed.

Systems and
Formalisms Lab