Week 4: Inductive Propositions and Inductive Reasoning

Display all goals and responses

Author: Aurèle Barrière, Adam Chlipala, Benjamin C. Pierce
License: No redistribution allowed (usage by permission in CS-428).

Introduction

So far, we've seen how to define Coq functions, and how to define simple propositions. Examples of propositions included equality (for instance, proving that the result of a function call is equal to something). But we've also been constructing propositions with quantifiers (exists, forall), conjunction, disjunction, implication...

In this lecture, we look at yet another way to define propositions: the inductive ones.

We'll see how to define these inductive propositions.
We'll see how these can be particularly convenient to express propositions that were not so easy to define using our previous tools.
We'll see how to reason about them, by case analysis, inversion or induction, generalizing the induction principles we've been using before.

Revisiting Eval

Remember the simple language of arithmetic expressions with variables defined in Week 1.

Notation var := string.

Inductive arith : Set :=
| Const (n : nat)
| Var (x : var)
| Plus (e1 e2 : arith)
| Times (e1 e2 : arith).

Example ex1 := Const 42.
Example ex2 := Plus (Const 1) (Times (Var "x") (Var "y")).

It was pretty easy to define natural semantics for these expressions with a simple function. Of course, to evaluate variables, we needed a "valuation", a function defining the value of each variable.

The result is a function. Coq can compute it.

Notation val := (var -> nat).

Fixpoint eval (vn: val) (e: arith) : nat :=
  match e with
  | Const n => n
  | Var v => vn v
  | Plus e1 e2 => eval vn e1 + eval vn e2
  | Times e1 e2 => eval vn e1 * eval vn e2
  end.

Example eval_example: nat :=
  (eval (fun _ => 0) (Plus (Const 58) (Const 12))).
Compute eval_example.= 70
: nat

If you have some experience in defining programming language semantics, you might be used to another style of definition, with horizontal bars. (Blackboard example). Let's try to write the same thing in Coq:

Inductive ieval: val -> arith -> nat -> Prop :=
| i_const:
  forall (vn:val) (n:nat),
    ieval vn (Const n) n
| i_var:
  forall (vn:val) (v:var) (n:nat)
    (EVAL_VAR: vn v = n),
    ieval vn (Var v) n
| i_plus:
  forall (vn:val) (e1 e2:arith) (n1 n2:nat)
    (EVAL_LEFT: ieval vn e1 n1)
    (EVAL_RIGHT: ieval vn e2 n2),
    ieval vn (Plus e1 e2) (n1 + n2)
| i_times:
  forall (vn:val) (e1 e2:arith) (n1 n2:nat)
    (EVAL_LEFT: ieval vn e1 n1)
    (EVAL_RIGHT: ieval vn e2 n2),
    ieval vn (Times e1 e2) (n1 * n2).

The process of turning the blackboard rules into Coq rules has been straightforward:

rule names become constructor names
hypotheses above the bar become universally quantified
conclusions below the bar are conclusions of each constructor.

Note that naming hypotheses is optional and could be replaced by an implication.

But what does this represent in Coq? We have just defined an inductive proposition (note the Inductive and Prop keywords). Just like a = b was a proposition, now ieval vn e n is a proposition.

What do we love to do with propositions? Prove them!

Lemma ieval_example:
  ieval (fun _ => 0) (Plus (Const 58) (Const 12)) 70.ieval (fun _ : var => 0) (Plus (Const 58) (Const 12))
  70
Proof.ieval (fun _ : var => 0) (Plus (Const 58) (Const 12))
  70
  (* each constructor can be applied, like a blackboard rule *)
  Fail apply i_plus.The command has indeed failed with message:
Unable to unify
 "ieval ?M1358 (Plus ?M1359 ?M1360) (?M1361 + ?M1362)"
with
 "ieval (fun _ : var => 0)
    (Plus (Const 58) (Const 12)) 70".
ieval (fun _ : var => 0) (Plus (Const 58) (Const 12))
  70
  (* the rule expects the Plus to evaluate to an addition,
     let's show that 70 is in fact an addition *)
  replace 70 with (58 + 12) by lia.ieval (fun _ : var => 0) (Plus (Const 58) (Const 12))
  (58 + 12)
  apply i_plus.ieval (fun _ : var => 0) (Const 58) 58
ieval (fun _ : var => 0) (Const 12) 12
  (* apply (i_plus _ _ _ 58 12). would have also worked *)
  (* our rule had two premises. we need to prove them both *)
  -ieval (fun _ : var => 0) (Const 58) 58 apply i_const.
  -ieval (fun _ : var => 0) (Const 12) 12 apply i_const.
Qed.

This is a start. But we can prove more interesting properties. For instance, let's prove the following property:

Theorem eval_implies_ieval:
  forall (vn:val) (e:arith) (n:nat),
    eval vn e = n -> ieval vn e n.forall (vn : val) (e : arith) (n : nat),
eval vn e = n -> ieval vn e n
Proof.forall (vn : val) (e : arith) (n : nat),
eval vn e = n -> ieval vn e n
  intros vn e.vn: val
e: arith
forall n : nat, eval vn e = n -> ieval vn e n
  induction e; intros; simpl in H.vn: val
n, n0: nat
H: n = n0
ieval vn (Const n) n0
vn: val
x: var
n: nat
H: vn x = n
ieval vn (Var x) n
vn: val
e1, e2: arith
IHe1: forall n : nat, eval vn e1 = n -> ieval vn e1 n
IHe2: forall n : nat, eval vn e2 = n -> ieval vn e2 n
n: nat
H: eval vn e1 + eval vn e2 = n
ieval vn (Plus e1 e2) n
vn: val
e1, e2: arith
IHe1: forall n : nat, eval vn e1 = n -> ieval vn e1 n
IHe2: forall n : nat, eval vn e2 = n -> ieval vn e2 n
n: nat
H: eval vn e1 * eval vn e2 = n
ieval vn (Times e1 e2) n
  -vn: val
n, n0: nat
H: n = n0
ieval vn (Const n) n0 subst.vn: val
n0: nat
ieval vn (Const n0) n0 apply i_const.
  -vn: val
x: var
n: nat
H: vn x = n
ieval vn (Var x) n apply i_var.vn: val
x: var
n: nat
H: vn x = n
vn x = n assumption.
  -vn: val
e1, e2: arith
IHe1: forall n : nat, eval vn e1 = n -> ieval vn e1 n
IHe2: forall n : nat, eval vn e2 = n -> ieval vn e2 n
n: nat
H: eval vn e1 + eval vn e2 = n
ieval vn (Plus e1 e2) n rewrite <- H.vn: val
e1, e2: arith
IHe1: forall n : nat, eval vn e1 = n -> ieval vn e1 n
IHe2: forall n : nat, eval vn e2 = n -> ieval vn e2 n
n: nat
H: eval vn e1 + eval vn e2 = n
ieval vn (Plus e1 e2) (eval vn e1 + eval vn e2) apply i_plus.vn: val
e1, e2: arith
IHe1: forall n : nat, eval vn e1 = n -> ieval vn e1 n
IHe2: forall n : nat, eval vn e2 = n -> ieval vn e2 n
n: nat
H: eval vn e1 + eval vn e2 = n
ieval vn e1 (eval vn e1)
vn: val
e1, e2: arith
IHe1: forall n : nat, eval vn e1 = n -> ieval vn e1 n
IHe2: forall n : nat, eval vn e2 = n -> ieval vn e2 n
n: nat
H: eval vn e1 + eval vn e2 = n
ieval vn e2 (eval vn e2)
    +vn: val
e1, e2: arith
IHe1: forall n : nat, eval vn e1 = n -> ieval vn e1 n
IHe2: forall n : nat, eval vn e2 = n -> ieval vn e2 n
n: nat
H: eval vn e1 + eval vn e2 = n
ieval vn e1 (eval vn e1) apply IHe1.vn: val
e1, e2: arith
IHe1: forall n : nat, eval vn e1 = n -> ieval vn e1 n
IHe2: forall n : nat, eval vn e2 = n -> ieval vn e2 n
n: nat
H: eval vn e1 + eval vn e2 = n
eval vn e1 = eval vn e1 reflexivity.
    +vn: val
e1, e2: arith
IHe1: forall n : nat, eval vn e1 = n -> ieval vn e1 n
IHe2: forall n : nat, eval vn e2 = n -> ieval vn e2 n
n: nat
H: eval vn e1 + eval vn e2 = n
ieval vn e2 (eval vn e2) apply IHe2.vn: val
e1, e2: arith
IHe1: forall n : nat, eval vn e1 = n -> ieval vn e1 n
IHe2: forall n : nat, eval vn e2 = n -> ieval vn e2 n
n: nat
H: eval vn e1 + eval vn e2 = n
eval vn e2 = eval vn e2 reflexivity.
  -vn: val
e1, e2: arith
IHe1: forall n : nat, eval vn e1 = n -> ieval vn e1 n
IHe2: forall n : nat, eval vn e2 = n -> ieval vn e2 n
n: nat
H: eval vn e1 * eval vn e2 = n
ieval vn (Times e1 e2) n rewrite <- H.vn: val
e1, e2: arith
IHe1: forall n : nat, eval vn e1 = n -> ieval vn e1 n
IHe2: forall n : nat, eval vn e2 = n -> ieval vn e2 n
n: nat
H: eval vn e1 * eval vn e2 = n
ieval vn (Times e1 e2) (eval vn e1 * eval vn e2) apply i_times.vn: val
e1, e2: arith
IHe1: forall n : nat, eval vn e1 = n -> ieval vn e1 n
IHe2: forall n : nat, eval vn e2 = n -> ieval vn e2 n
n: nat
H: eval vn e1 * eval vn e2 = n
ieval vn e1 (eval vn e1)
vn: val
e1, e2: arith
IHe1: forall n : nat, eval vn e1 = n -> ieval vn e1 n
IHe2: forall n : nat, eval vn e2 = n -> ieval vn e2 n
n: nat
H: eval vn e1 * eval vn e2 = n
ieval vn e2 (eval vn e2)
    +vn: val
e1, e2: arith
IHe1: forall n : nat, eval vn e1 = n -> ieval vn e1 n
IHe2: forall n : nat, eval vn e2 = n -> ieval vn e2 n
n: nat
H: eval vn e1 * eval vn e2 = n
ieval vn e1 (eval vn e1) apply IHe1.vn: val
e1, e2: arith
IHe1: forall n : nat, eval vn e1 = n -> ieval vn e1 n
IHe2: forall n : nat, eval vn e2 = n -> ieval vn e2 n
n: nat
H: eval vn e1 * eval vn e2 = n
eval vn e1 = eval vn e1 reflexivity.
    +vn: val
e1, e2: arith
IHe1: forall n : nat, eval vn e1 = n -> ieval vn e1 n
IHe2: forall n : nat, eval vn e2 = n -> ieval vn e2 n
n: nat
H: eval vn e1 * eval vn e2 = n
ieval vn e2 (eval vn e2) apply IHe2.vn: val
e1, e2: arith
IHe1: forall n : nat, eval vn e1 = n -> ieval vn e1 n
IHe2: forall n : nat, eval vn e2 = n -> ieval vn e2 n
n: nat
H: eval vn e1 * eval vn e2 = n
eval vn e2 = eval vn e2 reflexivity.
Qed.

(* let's make it a bit more automated *)
Theorem eval_implies_ieval':
  forall (vn:val) (e:arith) (n:nat),
    eval vn e = n -> ieval vn e n.forall (vn : val) (e : arith) (n : nat),
eval vn e = n -> ieval vn e n
Proof.forall (vn : val) (e : arith) (n : nat),
eval vn e = n -> ieval vn e n
  induction e; intros; subst; constructor; auto.
  (* constructor applies the first inductive rule it can apply! *)
Qed.

We could expect doing the other implication... but we'll wait a bit for now.

You might think this is a bit more painful than just writing the evaluation function, and for that particular case you may be right. But let's now consider some variations.

What if some of my variables are undefined? In my valuation function, we'll represent this with an option.

Notation valop := (var -> option nat).
Example vo:valop :=
  (fun v =>
     match v with
     | "x" => Some 17
     | "y" => Some 3
     | _ => None
     end).

What should be the behavior of arithmetic expressions containing such undefined variables? First, we could just say that the expression does not evaluate at all. In our functional version of eval, we could do this with an option (left as exercise).

What about our inductive proposition?

Inductive ioeval: valop -> arith -> nat -> Prop :=
| io_const:
  forall (vn:valop) (n:nat),
    ioeval vn (Const n) n
| io_var:
  forall (vn:valop) (v:var) (n:nat)
    (EVAL_VAR: vn v = Some n),  (* here we change to a Some *)
    ioeval vn (Var v) n
| io_plus:
  forall (vn:valop) (e1 e2:arith) (n1 n2:nat)
    (EVAL_LEFT: ioeval vn e1 n1)
    (EVAL_RIGHT: ioeval vn e2 n2),
    ioeval vn (Plus e1 e2) (n1 + n2)
| io_times:
  forall (vn:valop) (e1 e2:arith) (n1 n2:nat)
    (EVAL_LEFT: ioeval vn e1 n1)
    (EVAL_RIGHT: ioeval vn e2 n2),
    ioeval vn (Times e1 e2) (n1 * n2).

No further changes are needed. We simply did not give a meaning to variables v when vn v = None. The arithmetic expression has "blocking semantics", there is no way to construct a proof tree evaluating this expression to any value using that valuation. In fact we can even prove it.

Lemma blocking_sem:
  forall ret, ~ (ioeval vo (Var "z") ret).forall ret : nat, ~ ioeval vo (Var "z") ret
Proof.forall ret : nat, ~ ioeval vo (Var "z") ret
  unfold not.forall ret : nat, ioeval vo (Var "z") ret -> False intros.ret: nat
H: ioeval vo (Var "z") ret
False
  inversion H. (* what happened here? we'll discuss it soon *)ret: nat
H: ioeval vo (Var "z") ret
vn: valop
v: var
n: nat
EVAL_VAR: vo "z" = Some ret
H0: vn = vo
H2: v = "z"
H1: n = ret
False
  simpl in EVAL_VAR.ret: nat
H: ioeval vo (Var "z") ret
vn: valop
v: var
n: nat
EVAL_VAR: None = Some ret
H0: vn = vo
H2: v = "z"
H1: n = ret
False inversion EVAL_VAR.
Qed.

But now, consider another variation, non-determinism. Suppose that now, undefined variable may evaluate to any possible number! This would be difficult to define in the functional style of eval.

But how would you adapt the blackboard rules? We can do the same thing in our Coq inductive proposition:

Inductive ineval: valop -> arith -> nat -> Prop :=
| in_const:
  forall (vn:valop) (n:nat),
    ineval vn (Const n) n
| in_var:
  forall (vn:valop) (v:var) (n:nat)
    (EVAL_VAR: vn v = Some n),
    ineval vn (Var v) n
| in_undef:
  forall (vn:valop) (v:var) (n:nat)
    (UNDEFINED: vn v = None), (* for any possible n! *)
    ineval vn (Var v) n
| in_plus:
  forall (vn:valop) (e1 e2:arith) (n1 n2:nat)
    (EVAL_LEFT: ineval vn e1 n1)
    (EVAL_RIGHT: ineval vn e2 n2),
    ineval vn (Plus e1 e2) (n1 + n2)
| in_times:
  forall (vn:valop) (e1 e2:arith) (n1 n2:nat)
    (EVAL_LEFT: ineval vn e1 n1)
    (EVAL_RIGHT: ineval vn e2 n2),
    ineval vn (Times e1 e2) (n1 * n2).

We can now prove that a non-deterministic expression like (Var "z") has several meanings.

Lemma z_meaning1:
  ineval vo (Var "z") 623.ineval vo (Var "z") 623
Proof.ineval vo (Var "z") 623
  apply in_undef.vo "z" = None
  simpl.None = None reflexivity.
Qed.

Lemma z_meaning2:
  ineval vo (Var "z") 236236.To avoid stack overflow, large numbers in nat are
interpreted as applications of Init.Nat.of_num_uint.
[abstract-large-number,numbers,default]
ineval vo (Var "z")
  (Init.Nat.of_num_uint
     (Number.UIntDecimal
        (Decimal.D2
           (Decimal.D3
              (Decimal.D6
                 (Decimal.D2
                    (Decimal.D3
                       (Decimal.D6 Decimal.Nil))))))))
Proof.ineval vo (Var "z")
  (Init.Nat.of_num_uint
     (Number.UIntDecimal
        (Decimal.D2
           (Decimal.D3
              (Decimal.D6
                 (Decimal.D2
                    (Decimal.D3
                       (Decimal.D6 Decimal.Nil))))))))
  apply in_undef.vo "z" = None
  simpl.None = None reflexivity.
Qed.

Interestingly, we see that these inductive propositions are convenient to define

partial functions (instead of using an option type)
multi-valued functions (or non-deterministic)

In both cases, the idea is that we see such functions as mathematical relations between their input and their output. While Coq functions are expected to be total (each input has an output) and deterministic (only one output), this notion of relation can accommodate broader definitions. Of course, this expressivity comes at the cost of having a function that can actually be computed within Coq. But this is still convenient for models, invariant, semantics, specifications...

We also previously saw that Coq functions were expected to terminate. Is this also a restriction we can lift by using an inductive proposition?

Let us now leave our arithmetic expressions and consider the famous Collatz or Syracuse conjecture.

The Syracuse sequence computes the next natural number in the sequence as follows:

if k (the last number of the sequence) is equal to 1, the sequence is over
if k is even, divide it by 2 and call Syracuse recursively on the result
if k is odd, multiply it by 3, add 1 and call Syracuse recursively on the result.

The sequence is then determined by the first number. Starting from 12, we get the sequence 12, 6, 3, 10, 5, 16, 8, 4, 2, 1. Starting from 19, we get the sequence è19, 58, 29, 88, 44, 22, 11, 34, 17, 52, 26, 13, 40, 20, 10, 5, 16, 8, 4, 2, 1`.

The Collatz conjecture states that this sequence is always finite, in other words that 1 is always reached, for any starting natural number.

To formalize this conjecture in Coq, we might try to define a recursive function that calculates the total number of steps that it takes for such a sequence to reach 1.

(* next number in the Syracuse sequence *)
Definition next_syracuse (k : nat) :=
  if even k then div2 k
  else (3 * k) + 1.

Fixpoint reaches_1_in (n : nat) :=
  if Nat.eqb n 1 then 1
  else 1 + reaches_1_in (next_syracuse n).Recursive definition of reaches_1_in is ill-formed.
In environment
reaches_1_in : nat -> nat
n : nat
Recursive call to reaches_1_in has principal argument
equal to "next_syracuse n" instead of
a subterm of "n".
Recursive definition is:
"fun n : nat =>
 if (n =? 1)%nat
 then 1
 else 1 + reaches_1_in (next_syracuse n)".

This definition is rejected by Coq's termination checker, since the argument to the recursive call, next_syracuse n, is not "obviously smaller" than n.

Indeed, this isn't just a pointless limitation: functions in Coq are required to be total, to ensure logical consistency.

Moreover, we can't fix it by devising a more clever termination checker: deciding whether this particular function is total would be equivalent to settling the Collatz conjecture!

Fortunately, there is another way to do it: We can express the concept "reaches 1 eventually" as an inductively defined property of numbers:

Inductive Collatz_holds_for : nat -> Prop :=
  | Chf_done : Collatz_holds_for 1
  | Chf_more (n : nat) : Collatz_holds_for (next_syracuse n) ->
                       Collatz_holds_for n.

What we've done here is to use Coq's Inductive definition mechanism to characterize the property "Collatz holds for..." by stating two different ways in which it can hold: (1) Collatz holds for 1 and (2) if Collatz holds for next_syracuse n then it holds for n.

We can prove that indeed the Collatz conjecture holds for some numbers:

Example Collatz_holds_for_12 : Collatz_holds_for 12.Collatz_holds_for 12
Proof.Collatz_holds_for 12
  apply Chf_more.Collatz_holds_for (next_syracuse 12) unfold next_syracuse.Collatz_holds_for
  (if even 12 then div2 12 else 3 * 12 + 1) simpl.Collatz_holds_for 6
  apply Chf_more.Collatz_holds_for (next_syracuse 6) unfold next_syracuse.Collatz_holds_for
  (if even 6 then div2 6 else 3 * 6 + 1) simpl.Collatz_holds_for 3
  apply Chf_more.Collatz_holds_for (next_syracuse 3) unfold next_syracuse.Collatz_holds_for
  (if even 3 then div2 3 else 3 * 3 + 1) simpl.Collatz_holds_for 10
  apply Chf_more.Collatz_holds_for (next_syracuse 10) unfold next_syracuse.Collatz_holds_for
  (if even 10 then div2 10 else 3 * 10 + 1) simpl.Collatz_holds_for 5
  apply Chf_more.Collatz_holds_for (next_syracuse 5) unfold next_syracuse.Collatz_holds_for
  (if even 5 then div2 5 else 3 * 5 + 1) simpl.Collatz_holds_for 16
  apply Chf_more.Collatz_holds_for (next_syracuse 16) unfold next_syracuse.Collatz_holds_for
  (if even 16 then div2 16 else 3 * 16 + 1) simpl.Collatz_holds_for 8
  apply Chf_more.Collatz_holds_for (next_syracuse 8) unfold next_syracuse.Collatz_holds_for
  (if even 8 then div2 8 else 3 * 8 + 1) simpl.Collatz_holds_for 4
  apply Chf_more.Collatz_holds_for (next_syracuse 4) unfold next_syracuse.Collatz_holds_for
  (if even 4 then div2 4 else 3 * 4 + 1) simpl.Collatz_holds_for 2
  apply Chf_more.Collatz_holds_for (next_syracuse 2) unfold next_syracuse.Collatz_holds_for
  (if even 2 then div2 2 else 3 * 2 + 1) simpl.Collatz_holds_for 1
  apply Chf_done.  Qed.

Of course if you manage to prove the theorem below, I would be very impressed.

Theorem Collatz_Conjecture:
  forall n, Collatz_holds_for n.forall n : nat, Collatz_holds_for n
Proof.forall n : nat, Collatz_holds_for n
Admitted.

Taking A Step Back: Defining Inductive Propositions

You now have a methodology to define any kind of relations as inductive propositions. As we translated blackboard rules into Coq, you may have noted that the syntax was strangely similar to defining inductive datatypes. This is an important observation, that we'll reuse soon when doing proofs about inductive propositions.

If we think about the blackboard rules, whenever you use them to prove something, you build a "proof derivation" or a "proof tree". This proof tree itself looks like something we could describe with an inductive datatype! In some way, by defining the Coq inductive proposition, you defined the different ways to build the proof tree: it's as if you described the proof tree inductive type. Now, proving that some inductive proposition holds amounts to constructing a proof tree, or constructing an element of that inductive type you just defined.

In Coq, we can show the proofs object being constructed. Let's look at these proof trees for an example.

Example Collatz_holds_for_12' : Collatz_holds_for 12.Collatz_holds_for 12
Proof.Collatz_holds_for 12
  apply Chf_more; unfold next_syracuse; simpl.Collatz_holds_for 6 Show Proof.(Chf_more 12
   ((?Goal
     :
     Collatz_holds_for
       (if even 12 then div2 12 else 3 * 12 + 1))
    :
    Collatz_holds_for (next_syracuse 12)))
Collatz_holds_for 6
  apply Chf_more; unfold next_syracuse; simpl.Collatz_holds_for 3 Show Proof.(Chf_more 12
   ((Chf_more 6
       ((?Goal
         :
         Collatz_holds_for
           (if even 6 then div2 6 else 3 * 6 + 1))
        :
        Collatz_holds_for (next_syracuse 6))
     :
     Collatz_holds_for
       (if even 12 then div2 12 else 3 * 12 + 1))
    :
    Collatz_holds_for (next_syracuse 12)))
Collatz_holds_for 3
  apply Chf_more; unfold next_syracuse; simpl.Collatz_holds_for 10 Show Proof.(Chf_more 12
   ((Chf_more 6
       ((Chf_more 3
           ((?Goal
             :
             Collatz_holds_for
               (if even 3 then div2 3 else 3 * 3 + 1))
            :
            Collatz_holds_for (next_syracuse 3))
         :
         Collatz_holds_for
           (if even 6 then div2 6 else 3 * 6 + 1))
        :
        Collatz_holds_for (next_syracuse 6))
     :
     Collatz_holds_for
       (if even 12 then div2 12 else 3 * 12 + 1))
    :
    Collatz_holds_for (next_syracuse 12)))
Collatz_holds_for 10
  apply Chf_more; unfold next_syracuse; simpl.Collatz_holds_for 5 Show Proof.(Chf_more 12
   ((Chf_more 6
       ((Chf_more 3
           ((Chf_more 10
               ((?Goal
                 :
                 Collatz_holds_for
                   (if even 10
                    then div2 10
                    else 3 * 10 + 1))
                :
                Collatz_holds_for (next_syracuse 10))
             :
             Collatz_holds_for
               (if even 3 then div2 3 else 3 * 3 + 1))
            :
            Collatz_holds_for (next_syracuse 3))
         :
         Collatz_holds_for
           (if even 6 then div2 6 else 3 * 6 + 1))
        :
        Collatz_holds_for (next_syracuse 6))
     :
     Collatz_holds_for
       (if even 12 then div2 12 else 3 * 12 + 1))
    :
    Collatz_holds_for (next_syracuse 12)))
Collatz_holds_for 5
  apply Chf_more; unfold next_syracuse; simpl.Collatz_holds_for 16 Show Proof.(Chf_more 12
   ((Chf_more 6
       ((Chf_more 3
           ((Chf_more 10
               ((Chf_more 5
                   ((?Goal : Collatz_holds_for ...)
                    :
                    Collatz_holds_for
                      (next_syracuse 5))
                 :
                 Collatz_holds_for
                   (if even 10
                    then div2 10
                    else 3 * 10 + 1))
                :
                Collatz_holds_for (next_syracuse 10))
             :
             Collatz_holds_for
               (if even 3 then div2 3 else 3 * 3 + 1))
            :
            Collatz_holds_for (next_syracuse 3))
         :
         Collatz_holds_for
           (if even 6 then div2 6 else 3 * 6 + 1))
        :
        Collatz_holds_for (next_syracuse 6))
     :
     Collatz_holds_for
       (if even 12 then div2 12 else 3 * 12 + 1))
    :
    Collatz_holds_for (next_syracuse 12)))
Collatz_holds_for 16
  apply Chf_more; unfold next_syracuse; simpl.Collatz_holds_for 8 Show Proof.(Chf_more 12
   ((Chf_more 6
       ((Chf_more 3
           ((Chf_more 10
               ((Chf_more 5
                   ((Chf_more 16 ...
                     :
                     Collatz_holds_for ...)
                    :
                    Collatz_holds_for
                      (next_syracuse 5))
                 :
                 Collatz_holds_for
                   (if even 10
                    then div2 10
                    else 3 * 10 + 1))
                :
                Collatz_holds_for (next_syracuse 10))
             :
             Collatz_holds_for
               (if even 3 then div2 3 else 3 * 3 + 1))
            :
            Collatz_holds_for (next_syracuse 3))
         :
         Collatz_holds_for
           (if even 6 then div2 6 else 3 * 6 + 1))
        :
        Collatz_holds_for (next_syracuse 6))
     :
     Collatz_holds_for
       (if even 12 then div2 12 else 3 * 12 + 1))
    :
    Collatz_holds_for (next_syracuse 12)))
Collatz_holds_for 8
  apply Chf_more; unfold next_syracuse; simpl.Collatz_holds_for 4 Show Proof.(Chf_more 12
   ((Chf_more 6
       ((Chf_more 3
           ((Chf_more 10
               ((Chf_more 5
                   ((Chf_more 16 ...
                     :
                     Collatz_holds_for ...)
                    :
                    Collatz_holds_for
                      (next_syracuse 5))
                 :
                 Collatz_holds_for
                   (if even 10
                    then div2 10
                    else 3 * 10 + 1))
                :
                Collatz_holds_for (next_syracuse 10))
             :
             Collatz_holds_for
               (if even 3 then div2 3 else 3 * 3 + 1))
            :
            Collatz_holds_for (next_syracuse 3))
         :
         Collatz_holds_for
           (if even 6 then div2 6 else 3 * 6 + 1))
        :
        Collatz_holds_for (next_syracuse 6))
     :
     Collatz_holds_for
       (if even 12 then div2 12 else 3 * 12 + 1))
    :
    Collatz_holds_for (next_syracuse 12)))
Collatz_holds_for 4
  apply Chf_more; unfold next_syracuse; simpl.Collatz_holds_for 2 Show Proof.(Chf_more 12
   ((Chf_more 6
       ((Chf_more 3
           ((Chf_more 10
               ((Chf_more 5
                   ((Chf_more 16 ...
                     :
                     Collatz_holds_for ...)
                    :
                    Collatz_holds_for
                      (next_syracuse 5))
                 :
                 Collatz_holds_for
                   (if even 10
                    then div2 10
                    else 3 * 10 + 1))
                :
                Collatz_holds_for (next_syracuse 10))
             :
             Collatz_holds_for
               (if even 3 then div2 3 else 3 * 3 + 1))
            :
            Collatz_holds_for (next_syracuse 3))
         :
         Collatz_holds_for
           (if even 6 then div2 6 else 3 * 6 + 1))
        :
        Collatz_holds_for (next_syracuse 6))
     :
     Collatz_holds_for
       (if even 12 then div2 12 else 3 * 12 + 1))
    :
    Collatz_holds_for (next_syracuse 12)))
Collatz_holds_for 2
  apply Chf_more; unfold next_syracuse; simpl.Collatz_holds_for 1 Show Proof.(Chf_more 12
   ((Chf_more 6
       ((Chf_more 3
           ((Chf_more 10
               ((Chf_more 5
                   ((Chf_more 16 ...
                     :
                     Collatz_holds_for ...)
                    :
                    Collatz_holds_for
                      (next_syracuse 5))
                 :
                 Collatz_holds_for
                   (if even 10
                    then div2 10
                    else 3 * 10 + 1))
                :
                Collatz_holds_for (next_syracuse 10))
             :
             Collatz_holds_for
               (if even 3 then div2 3 else 3 * 3 + 1))
            :
            Collatz_holds_for (next_syracuse 3))
         :
         Collatz_holds_for
           (if even 6 then div2 6 else 3 * 6 + 1))
        :
        Collatz_holds_for (next_syracuse 6))
     :
     Collatz_holds_for
       (if even 12 then div2 12 else 3 * 12 + 1))
    :
    Collatz_holds_for (next_syracuse 12)))
Collatz_holds_for 1
  apply Chf_done.  Qed.

Now, let's familiarize ourselves with some more inductive propositions. We can use them to represent sets!

Inductive my_favorite_numbers : nat -> Prop :=
| ILike17 : my_favorite_numbers 17
| ILike23 : my_favorite_numbers 23
| ILike28 : my_favorite_numbers 28.

Let's a pick a simple relation between natural numbers: being strictly less than another number.

Inductive lt: nat -> nat -> Prop :=
| lt_next: forall n, lt n (S n)
| lt_skip: forall n m (LT: lt n m), lt n (S m).

Lemma lt36:
  lt 3 6.lt 3 6
Proof.lt 3 6
  apply lt_skip.lt 3 5 apply lt_skip.lt 3 4 apply lt_next.
Qed.

In fact, this lt relation can be seen as the transitive closure of another relation, relating numbers that are off by one (for instance, 4 and 5). We can similarly define this notion of transitive closure as an inductive proposition.

(* TC : Transitive Closure *)
Inductive tc {A} (R : A -> A -> Prop) : A -> A -> Prop :=
| TcBase : forall x y, R x y -> tc R x y
| TcTrans : forall x y z, tc R x y -> tc R y z -> tc R x z.

Let's redefine lt now as a transitive closure.

Definition oneApart (n m : nat) : Prop :=
  n + 1 = m.

Definition lt' : nat -> nat -> Prop := tc oneApart.

Let's see another use of the transitive closure: parent relationships. Let's define a family with their parent relationships.

Inductive person : Type :=
| Hera
| Ares
| Hephaestus
| Eros.

Inductive parent_of: person -> person -> Prop :=
| he_ar: parent_of Hera Ares
| he_he: parent_of Hera Hephaestus
| ar_er: parent_of Ares Eros.

Definition ancestor_of : person -> person -> Prop :=
  tc parent_of.

Example ancestor_of1 : ancestor_of Hera Eros.ancestor_of Hera Eros
Proof.ancestor_of Hera Eros
  unfold ancestor_of.tc parent_of Hera Eros apply TcTrans with Ares.tc parent_of Hera Ares
tc parent_of Ares Eros
  -tc parent_of Hera Ares apply TcBase.parent_of Hera Ares apply he_ar.
  -tc parent_of Ares Eros apply TcBase.parent_of Ares Eros apply ar_er.
Qed.

Useless question: what do you think is the simplest way to define an inductive proposition that never holds? And an inductive relation that always hold?

Inductive useless: nat -> Prop := .

Inductive total_relation : nat -> nat -> Prop :=
  | tot n m : total_relation n m.

One last example: we can define what it means for natural numbers to be even. Of course there are many equivalent definitions.

Inductive ev : nat -> Prop :=
  | ev_0: ev 0
  | ev_SS (n : nat) (H : ev n) : ev (S (S n)).

Inductive Reasoning

By defining our inductive propositions with rules, we've not only a way to construct evidence that a property holds, using each rule as a theorem. We've also established that the only way for the property to hold is by having a proof tree using only these inductive constructors.

This is a very strong observation when conducting proofs with inductive propositions!

Defining ev with an Inductive declaration tells Coq not only that the constructors ev_0 and ev_SS are valid ways to build evidence that some number is ev, but also that these two constructors are the only ways to build evidence that numbers are ev.

To go back to the inductive types comparison, similarly every list is either a nil list or the concatenation of some elements to some other list.

This means that, just like on inductive types, we can destruct and do induction on the proof trees of inductive propositions!

So we can for instance prove the following lemma!

Theorem ev_inversion : forall (n : nat),
    ev n ->
    (n = 0) \/ (exists n', n = S (S n') /\ ev n').forall n : nat,
ev n ->
n = 0 \/ (exists n' : nat, n = S (S n') /\ ev n')
Proof.forall n : nat,
ev n ->
n = 0 \/ (exists n' : nat, n = S (S n') /\ ev n')
  intros n E.n: nat
E: ev n
n = 0 \/ (exists n' : nat, n = S (S n') /\ ev n')  destruct E as [ | n' E'] eqn:EE.E: ev 0
EE: E = ev_0
0 = 0 \/ (exists n' : nat, 0 = S (S n') /\ ev n')
n': nat
E: ev (S (S n'))
E': ev n'
EE: E = ev_SS n' E'
S (S n') = 0 \/
(exists n'0 : nat, S (S n') = S (S n'0) /\ ev n'0)
  - (* E = ev_0 : ev 0 *)E: ev 0
EE: E = ev_0
0 = 0 \/ (exists n' : nat, 0 = S (S n') /\ ev n')
    left.E: ev 0
EE: E = ev_0
0 = 0 reflexivity.
  - (* E = ev_SS n' E' : ev (S (S n')) *)n': nat
E: ev (S (S n'))
E': ev n'
EE: E = ev_SS n' E'
S (S n') = 0 \/
(exists n'0 : nat, S (S n') = S (S n'0) /\ ev n'0)
    right.n': nat
E: ev (S (S n'))
E': ev n'
EE: E = ev_SS n' E'
exists n'0 : nat, S (S n') = S (S n'0) /\ ev n'0 exists n'.n': nat
E: ev (S (S n'))
E': ev n'
EE: E = ev_SS n' E'
S (S n') = S (S n') /\ ev n' split.n': nat
E: ev (S (S n'))
E': ev n'
EE: E = ev_SS n' E'
S (S n') = S (S n')
n': nat
E: ev (S (S n'))
E': ev n'
EE: E = ev_SS n' E'
ev n' reflexivity.n': nat
E: ev (S (S n'))
E': ev n'
EE: E = ev_SS n' E'
ev n' apply E'.
Qed.

Facts like this are often called "inversion lemmas" because they allow us to "invert" some given information to reason about all the different ways it could have been derived.

Here, there are two ways to prove ev n, and the inversion lemma makes this explicit.

We can use the inversion lemma that we proved above to help structure proofs:

Theorem evSS_ev : forall n, ev (S (S n)) -> ev n.forall n : nat, ev (S (S n)) -> ev n
Proof.forall n : nat, ev (S (S n)) -> ev n
  intros n H.n: nat
H: ev (S (S n))
ev n apply ev_inversion in H.n: nat
H: S (S n) = 0 \/
(exists n' : nat, S (S n) = S (S n') /\ ev n')
ev n  destruct H as [H0|H1].n: nat
H0: S (S n) = 0
ev n
n: nat
H1: exists n' : nat, S (S n) = S (S n') /\ ev n'
ev n
  -n: nat
H0: S (S n) = 0
ev n discriminate H0.
  -n: nat
H1: exists n' : nat, S (S n) = S (S n') /\ ev n'
ev n destruct H1 as [n' [Hnm Hev]].n, n': nat
Hnm: S (S n) = S (S n')
Hev: ev n'
ev n injection Hnm as Heq.n, n': nat
Heq: n = n'
Hev: ev n'
ev n
    rewrite Heq.n, n': nat
Heq: n = n'
Hev: ev n'
ev n' apply Hev.
Qed.

But this such a common reasoning pattern that Coq provides a handy tactic called inversion that factors it out, saving us the trouble of explicitly stating and proving an inversion lemma for every Inductive definition we make.

Here, the inversion tactic can detect (1) that the first case, where n = 0, does not apply and (2) that the n' that appears in the ev_SS case must be the same as n. It includes an as annotation similar to destruct, allowing us to assign names rather than have Coq choose them.

Theorem evSS_ev' : forall n,
  ev (S (S n)) -> ev n.forall n : nat, ev (S (S n)) -> ev n
Proof.forall n : nat, ev (S (S n)) -> ev n
  intros n E.n: nat
E: ev (S (S n))
ev n  inversion E as [| n' E' Heq].n: nat
E: ev (S (S n))
n': nat
E': ev n
Heq: n' = n
ev n
  (* We are in the [E = ev_SS n' E'] case now. *)
  apply E'.
Qed.

Some more examples proofs with inversion:

Theorem one_not_even' : ~ ev 1.~ ev 1
Proof.~ ev 1
  intros H.H: ev 1
False inversion H. Qed.

Theorem favorites_below_50 : forall n, my_favorite_numbers n -> n < 50.forall n : nat, my_favorite_numbers n -> n < 50
Proof.forall n : nat, my_favorite_numbers n -> n < 50
  intros n H.n: nat
H: my_favorite_numbers n
n < 50
  inversion H.n: nat
H: my_favorite_numbers n
H0: 17 = n
17 < 50
n: nat
H: my_favorite_numbers n
H0: 23 = n
23 < 50
n: nat
H: my_favorite_numbers n
H0: 28 = n
28 < 50
  -n: nat
H: my_favorite_numbers n
H0: 17 = n
17 < 50 lia.
  -n: nat
H: my_favorite_numbers n
H0: 23 = n
23 < 50 lia.
  -n: nat
H: my_favorite_numbers n
H0: 28 = n
28 < 50 lia.
Qed.

Theorem SSSSev__even : forall n,
  ev (S (S (S (S n)))) -> ev n.forall n : nat, ev (S (S (S (S n)))) -> ev n
Proof.forall n : nat, ev (S (S (S (S n)))) -> ev n
  intros n E.n: nat
E: ev (S (S (S (S n))))
ev n  inversion E as [| n' E' EQ'].n: nat
E: ev (S (S (S (S n))))
n': nat
E': ev (S (S n))
EQ': n' = S (S n)
ev n
  inversion E' as [| n'' E'' EQ''].n: nat
E: ev (S (S (S (S n))))
n': nat
E': ev (S (S n))
EQ': n' = S (S n)
n'': nat
E'': ev n
EQ'': n'' = n
ev n  apply E''.
Qed.

The inversion tactic does quite a bit of work. For example, when applied to an equality assumption, it does the work of both discriminate and injection. In addition, it carries out the intros and rewrite`s that are typically necessary in the case of `injection. It can also be applied to analyze evidence for arbitrary inductively defined propositions, not just equality.

The tactic inversion actually works on any H : P where P is defined inductively:

For each constructor of P, make a subgoal where H is constrained by the form of this constructor.
Discard contradictory subgoals (such as ev_0 above).
Generate auxiliary equalities (as with ev_SS above).

But let's go even further. Just like we've seen that we can define a principle of induction on any inductive datatype, without surprise we can do inductive reasoning on the proof trees of inductive propositions!

The behavior of induction on evidence (or proof tree) is the same as its behavior on data: It causes Coq to generate one subgoal for each constructor that could have used to build that evidence, while providing an induction hypothesis for each recursive occurrence of the property in question.

Let's revisit our two definitions of eval and their equivalence;

Theorem ieval_implies_eval:
  forall (vn:val) (e:arith) (n:nat),
    ieval vn e n -> eval vn e = n.forall (vn : val) (e : arith) (n : nat),
ieval vn e n -> eval vn e = n
Proof.forall (vn : val) (e : arith) (n : nat),
ieval vn e n -> eval vn e = n
  intros vn e.vn: val
e: arith
forall n : nat, ieval vn e n -> eval vn e = n induction e; intros;
    inversion H; subst; simpl; try reflexivity.vn: val
e1, e2: arith
IHe1: forall n : nat, ieval vn e1 n -> eval vn e1 = n
IHe2: forall n : nat, ieval vn e2 n -> eval vn e2 = n
n1, n2: nat
H: ieval vn (Plus e1 e2) (n1 + n2)
EVAL_LEFT: ieval vn e1 n1
EVAL_RIGHT: ieval vn e2 n2
eval vn e1 + eval vn e2 = n1 + n2
vn: val
e1, e2: arith
IHe1: forall n : nat, ieval vn e1 n -> eval vn e1 = n
IHe2: forall n : nat, ieval vn e2 n -> eval vn e2 = n
n1, n2: nat
H: ieval vn (Times e1 e2) (n1 * n2)
EVAL_LEFT: ieval vn e1 n1
EVAL_RIGHT: ieval vn e2 n2
eval vn e1 * eval vn e2 = n1 * n2
  -vn: val
e1, e2: arith
IHe1: forall n : nat, ieval vn e1 n -> eval vn e1 = n
IHe2: forall n : nat, ieval vn e2 n -> eval vn e2 = n
n1, n2: nat
H: ieval vn (Plus e1 e2) (n1 + n2)
EVAL_LEFT: ieval vn e1 n1
EVAL_RIGHT: ieval vn e2 n2
eval vn e1 + eval vn e2 = n1 + n2 apply IHe1 in EVAL_LEFT.vn: val
e1, e2: arith
IHe1: forall n : nat, ieval vn e1 n -> eval vn e1 = n
IHe2: forall n : nat, ieval vn e2 n -> eval vn e2 = n
n1, n2: nat
H: ieval vn (Plus e1 e2) (n1 + n2)
EVAL_LEFT: eval vn e1 = n1
EVAL_RIGHT: ieval vn e2 n2
eval vn e1 + eval vn e2 = n1 + n2 apply IHe2 in EVAL_RIGHT.vn: val
e1, e2: arith
IHe1: forall n : nat, ieval vn e1 n -> eval vn e1 = n
IHe2: forall n : nat, ieval vn e2 n -> eval vn e2 = n
n1, n2: nat
H: ieval vn (Plus e1 e2) (n1 + n2)
EVAL_LEFT: eval vn e1 = n1
EVAL_RIGHT: eval vn e2 = n2
eval vn e1 + eval vn e2 = n1 + n2
    rewrite EVAL_LEFT.vn: val
e1, e2: arith
IHe1: forall n : nat, ieval vn e1 n -> eval vn e1 = n
IHe2: forall n : nat, ieval vn e2 n -> eval vn e2 = n
n1, n2: nat
H: ieval vn (Plus e1 e2) (n1 + n2)
EVAL_LEFT: eval vn e1 = n1
EVAL_RIGHT: eval vn e2 = n2
n1 + eval vn e2 = n1 + n2 rewrite EVAL_RIGHT.vn: val
e1, e2: arith
IHe1: forall n : nat, ieval vn e1 n -> eval vn e1 = n
IHe2: forall n : nat, ieval vn e2 n -> eval vn e2 = n
n1, n2: nat
H: ieval vn (Plus e1 e2) (n1 + n2)
EVAL_LEFT: eval vn e1 = n1
EVAL_RIGHT: eval vn e2 = n2
n1 + n2 = n1 + n2 reflexivity.
  -vn: val
e1, e2: arith
IHe1: forall n : nat, ieval vn e1 n -> eval vn e1 = n
IHe2: forall n : nat, ieval vn e2 n -> eval vn e2 = n
n1, n2: nat
H: ieval vn (Times e1 e2) (n1 * n2)
EVAL_LEFT: ieval vn e1 n1
EVAL_RIGHT: ieval vn e2 n2
eval vn e1 * eval vn e2 = n1 * n2 apply IHe1 in EVAL_LEFT.vn: val
e1, e2: arith
IHe1: forall n : nat, ieval vn e1 n -> eval vn e1 = n
IHe2: forall n : nat, ieval vn e2 n -> eval vn e2 = n
n1, n2: nat
H: ieval vn (Times e1 e2) (n1 * n2)
EVAL_LEFT: eval vn e1 = n1
EVAL_RIGHT: ieval vn e2 n2
eval vn e1 * eval vn e2 = n1 * n2 apply IHe2 in EVAL_RIGHT.vn: val
e1, e2: arith
IHe1: forall n : nat, ieval vn e1 n -> eval vn e1 = n
IHe2: forall n : nat, ieval vn e2 n -> eval vn e2 = n
n1, n2: nat
H: ieval vn (Times e1 e2) (n1 * n2)
EVAL_LEFT: eval vn e1 = n1
EVAL_RIGHT: eval vn e2 = n2
eval vn e1 * eval vn e2 = n1 * n2
    rewrite EVAL_LEFT.vn: val
e1, e2: arith
IHe1: forall n : nat, ieval vn e1 n -> eval vn e1 = n
IHe2: forall n : nat, ieval vn e2 n -> eval vn e2 = n
n1, n2: nat
H: ieval vn (Times e1 e2) (n1 * n2)
EVAL_LEFT: eval vn e1 = n1
EVAL_RIGHT: eval vn e2 = n2
n1 * eval vn e2 = n1 * n2 rewrite EVAL_RIGHT.vn: val
e1, e2: arith
IHe1: forall n : nat, ieval vn e1 n -> eval vn e1 = n
IHe2: forall n : nat, ieval vn e2 n -> eval vn e2 = n
n1, n2: nat
H: ieval vn (Times e1 e2) (n1 * n2)
EVAL_LEFT: eval vn e1 = n1
EVAL_RIGHT: eval vn e2 = n2
n1 * n2 = n1 * n2 reflexivity.
Qed.

Now with an induction on ieval:

Theorem ieval_implies_eval':
  forall (vn:val) (e:arith) (n:nat),
    ieval vn e n -> eval vn e = n.forall (vn : val) (e : arith) (n : nat),
ieval vn e n -> eval vn e = n
Proof.forall (vn : val) (e : arith) (n : nat),
ieval vn e n -> eval vn e = n
  intros vn e n H.vn: val
e: arith
n: nat
H: ieval vn e n
eval vn e = n induction H; simpl.vn: val
n: nat
n = n
vn: val
v: var
n: nat
EVAL_VAR: vn v = n
vn v = n
vn: val
e1, e2: arith
n1, n2: nat
H: ieval vn e1 n1
H0: ieval vn e2 n2
IHieval1: eval vn e1 = n1
IHieval2: eval vn e2 = n2
eval vn e1 + eval vn e2 = n1 + n2
vn: val
e1, e2: arith
n1, n2: nat
H: ieval vn e1 n1
H0: ieval vn e2 n2
IHieval1: eval vn e1 = n1
IHieval2: eval vn e2 = n2
eval vn e1 * eval vn e2 = n1 * n2
  -vn: val
n: nat
n = n reflexivity.
  -vn: val
v: var
n: nat
EVAL_VAR: vn v = n
vn v = n assumption.
  -vn: val
e1, e2: arith
n1, n2: nat
H: ieval vn e1 n1
H0: ieval vn e2 n2
IHieval1: eval vn e1 = n1
IHieval2: eval vn e2 = n2
eval vn e1 + eval vn e2 = n1 + n2 rewrite IHieval1.vn: val
e1, e2: arith
n1, n2: nat
H: ieval vn e1 n1
H0: ieval vn e2 n2
IHieval1: eval vn e1 = n1
IHieval2: eval vn e2 = n2
n1 + eval vn e2 = n1 + n2 rewrite IHieval2.vn: val
e1, e2: arith
n1, n2: nat
H: ieval vn e1 n1
H0: ieval vn e2 n2
IHieval1: eval vn e1 = n1
IHieval2: eval vn e2 = n2
n1 + n2 = n1 + n2 reflexivity.
  -vn: val
e1, e2: arith
n1, n2: nat
H: ieval vn e1 n1
H0: ieval vn e2 n2
IHieval1: eval vn e1 = n1
IHieval2: eval vn e2 = n2
eval vn e1 * eval vn e2 = n1 * n2 rewrite IHieval1.vn: val
e1, e2: arith
n1, n2: nat
H: ieval vn e1 n1
H0: ieval vn e2 n2
IHieval1: eval vn e1 = n1
IHieval2: eval vn e2 = n2
n1 * eval vn e2 = n1 * n2 rewrite IHieval2.vn: val
e1, e2: arith
n1, n2: nat
H: ieval vn e1 n1
H0: ieval vn e2 n2
IHieval1: eval vn e1 = n1
IHieval2: eval vn e2 = n2
n1 * n2 = n1 * n2 reflexivity.
Qed.

(* a bit simpler: *)
Theorem ieval_implies_eval'':
  forall (vn:val) (e:arith) (n:nat),
    ieval vn e n -> eval vn e = n.forall (vn : val) (e : arith) (n : nat),
ieval vn e n -> eval vn e = n
Proof.forall (vn : val) (e : arith) (n : nat),
ieval vn e n -> eval vn e = n
  induction 1; simpl; auto.
Qed.

Even though we got to the same result by doing either an induction on an element of an inductive type or an induction on the inductive proposition, it's important to understand that we are doing two entirely different proofs. Let's see an example with ev.

Theorem ev_ev__ev : forall n m,
  ev (n+m) -> ev n -> ev m.forall n m : nat, ev (n + m) -> ev n -> ev m
Proof.forall n m : nat, ev (n + m) -> ev n -> ev m
  induction n; intros.m: nat
H: ev (0 + m)
H0: ev 0
ev m
n: nat
IHn: forall m : nat, ev (n + m) -> ev n -> ev m
m: nat
H: ev (S n + m)
H0: ev (S n)
ev m
  -m: nat
H: ev (0 + m)
H0: ev 0
ev m simpl in H.m: nat
H: ev m
H0: ev 0
ev m assumption.
  -n: nat
IHn: forall m : nat, ev (n + m) -> ev n -> ev m
m: nat
H: ev (S n + m)
H0: ev (S n)
ev m
    apply IHn.n: nat
IHn: forall m : nat, ev (n + m) -> ev n -> ev m
m: nat
H: ev (S n + m)
H0: ev (S n)
ev (n + m)
n: nat
IHn: forall m : nat, ev (n + m) -> ev n -> ev m
m: nat
H: ev (S n + m)
H0: ev (S n)
ev n

This induction hypothesis does not seem helpful at all.

Abort.

Theorem ev_ev__ev : forall n m,
  ev (n+m) -> ev n -> ev m.forall n m : nat, ev (n + m) -> ev n -> ev m
Proof.forall n m : nat, ev (n + m) -> ev n -> ev m
  intros n m.n, m: nat
ev (n + m) -> ev n -> ev m generalize dependent n.m: nat
forall n : nat, ev (n + m) -> ev n -> ev m
  induction m; intros.n: nat
H: ev (n + 0)
H0: ev n
ev 0
m: nat
IHm: forall n : nat, ev (n + m) -> ev n -> ev m
n: nat
H: ev (n + S m)
H0: ev n
ev (S m)
  -n: nat
H: ev (n + 0)
H0: ev n
ev 0 constructor.
  -m: nat
IHm: forall n : nat, ev (n + m) -> ev n -> ev m
n: nat
H: ev (n + S m)
H0: ev n
ev (S m)

I don't have anything in my context to prove ev (S m)…

Abort.

(* OK I get it, you want me to use induction on a prop: *)
Theorem ev_ev__ev : forall n m,
  ev (n+m) -> ev n -> ev m.forall n m : nat, ev (n + m) -> ev n -> ev m
Proof.forall n m : nat, ev (n + m) -> ev n -> ev m
  intros n m Hnm.n, m: nat
Hnm: ev (n + m)
ev n -> ev m
  Fail solve[induction Hnm].The command has indeed failed with message:
No applicable tactic.
n, m: nat
Hnm: ev (n + m)
ev n -> ev m
  (* it seems like we lose the information that n+m is 0... *)
  remember (n+m) as nm.n, m, nm: nat
Heqnm: nm = n + m
Hnm: ev nm
ev n -> ev m
  (* otherwise it gets discarded *)
  induction Hnm; intros Hn.n, m: nat
Heqnm: 0 = n + m
Hn: ev n
ev m
n, m, n0: nat
Heqnm: S (S n0) = n + m
Hnm: ev n0
IHHnm: n0 = n + m -> ev n -> ev m
Hn: ev n
ev m
  -n, m: nat
Heqnm: 0 = n + m
Hn: ev n
ev m destruct m.n: nat
Heqnm: 0 = n + 0
Hn: ev n
ev 0
n, m: nat
Heqnm: 0 = n + S m
Hn: ev n
ev (S m)
    +n: nat
Heqnm: 0 = n + 0
Hn: ev n
ev 0 constructor.
    +n, m: nat
Heqnm: 0 = n + S m
Hn: ev n
ev (S m) rewrite add_succ_r in Heqnm.n, m: nat
Heqnm: 0 = S (n + m)
Hn: ev n
ev (S m) inversion Heqnm.
  -n, m, n0: nat
Heqnm: S (S n0) = n + m
Hnm: ev n0
IHHnm: n0 = n + m -> ev n -> ev m
Hn: ev n
ev m
    apply IHHnm.n, m, n0: nat
Heqnm: S (S n0) = n + m
Hnm: ev n0
IHHnm: n0 = n + m -> ev n -> ev m
Hn: ev n
n0 = n + m
n, m, n0: nat
Heqnm: S (S n0) = n + m
Hnm: ev n0
IHHnm: n0 = n + m -> ev n -> ev m
Hn: ev n
ev n

I'm still lost.

Abort.

Actually, not only do we have to be careful about induction on a value vs induction on a proposition but also, induction on different propositions are different proofs: choose the right one!

Theorem ev_ev__ev : forall n m,
    ev (n+m) -> ev n -> ev m.forall n m : nat, ev (n + m) -> ev n -> ev m
Proof.forall n m : nat, ev (n + m) -> ev n -> ev m
  intros n m Enm En.n, m: nat
Enm: ev (n + m)
En: ev n
ev m
  induction En as [| n' En'].m: nat
Enm: ev (0 + m)
ev m
m, n': nat
Enm: ev (S (S n') + m)
En': ev n'
IHEn': ev (n' + m) -> ev m
ev m
  - (* En = ev_0 *)m: nat
Enm: ev (0 + m)
ev m
    simpl in Enm.m: nat
Enm: ev m
ev m apply Enm.
  - (* En = ev_SS *)m, n': nat
Enm: ev (S (S n') + m)
En': ev n'
IHEn': ev (n' + m) -> ev m
ev m
    simpl in Enm.m, n': nat
Enm: ev (S (S (n' + m)))
En': ev n'
IHEn': ev (n' + m) -> ev m
ev m inversion Enm.m, n': nat
Enm: ev (S (S (n' + m)))
En': ev n'
IHEn': ev (n' + m) -> ev m
n: nat
H0: ev (n' + m)
H: n = n' + m
ev m apply IHEn'.m, n': nat
Enm: ev (S (S (n' + m)))
En': ev n'
IHEn': ev (n' + m) -> ev m
n: nat
H0: ev (n' + m)
H: n = n' + m
ev (n' + m) apply H0.
Qed.

Maybe there's a lesson here... Doing induction on random things may not be the best proof strategy.

Every time we define an inductive proposition, Coq creates an induction principle:

(* just like for inductive types: *)
Check nat_ind.nat_ind
     : forall P : nat -> Prop,
       P 0 ->
       (forall n : nat, P n -> P (S n)) ->
       forall n : nat, P n
(* for inductive propositions: *)
Check useless_ind.useless_ind
     : forall (P : nat -> Prop) (n : nat),
       useless n -> P n
Check total_relation_ind.total_relation_ind
     : forall P : nat -> nat -> Prop,
       (forall n m : nat, P n m) ->
       forall n n0 : nat,
       total_relation n n0 -> P n n0
Check lt_ind.lt_ind
     : forall P : nat -> nat -> Prop,
       (forall n : nat, P n (S n)) ->
       (forall n m : nat, lt n m -> P n m -> P n (S m)) ->
       forall n n0 : nat, lt n n0 -> P n n0
Check ieval_ind.ieval_ind
     : forall P : val -> arith -> nat -> Prop,
       (forall (vn : val) (n : nat), P vn (Const n) n) ->
       (forall (vn : val) (v : var) (n : nat),
        vn v = n -> P vn (Var v) n) ->
       (forall (vn : val) (e1 e2 : arith)
          (n1 n2 : nat),
        ieval vn e1 n1 ->
        P vn e1 n1 ->
        ieval vn e2 n2 ->
        P vn e2 n2 -> P vn (Plus e1 e2) (n1 + n2)) ->
       (forall (vn : val) (e1 e2 : arith)
          (n1 n2 : nat),
        ieval vn e1 n1 ->
        P vn e1 n1 ->
        ieval vn e2 n2 ->
        P vn e2 n2 -> P vn (Times e1 e2) (n1 * n2)) ->
       forall (n : val) (a : arith) (n0 : nat),
       ieval n a n0 -> P n a n0
Check parent_of_ind.parent_of_ind
     : forall P : person -> person -> Prop,
       P Hera Ares ->
       P Hera Hephaestus ->
       P Ares Eros ->
       forall p p0 : person, parent_of p p0 -> P p p0

Systems and
Formalisms Lab