How to perform induction over two inductive predicates?

Question

I am starting with Coq and trying to formalize Automated Amortised Analysis. I am at lemma 4.13:

Lemma preservation : forall (Sigma : prog_sig) (Gamma : context) (p : program)
  (s : stack) (h h' : heap) (e : expr) (c : type0) (v : val),
  (* 4.1 *) has_type Sigma Gamma e c ->
  (* 4.2 *) eval p s h e v h' ->
  (* 4.3 *) mem_consistant_stack h s Gamma ->
  (* 4.a *) mem_consistant h' v c /\ (* 4.b *) mem_consistant_stack h' s Gamma.
Proof.
  intros Sigma Gamma p s h h' e c v WELL_TYPED EVAL.

The manual proof uses a double induction:

Proof. Note that claim (4.b) follows directly by Lemma 4.8 and Lemma 4.12. Each location l ∈ dom( H ) is either left unaltered or is overwritten by the value Bad and hence does not invalidate memory consistency.

However, the first claim (4.a) requires a proof by induction on the lengths of the derivations of (4.2) and (4.1) ordered lexicographically with the derivation of the evaluation taking priority over the typing derivation. This is required since an in- duction on the length of the typing derivation alone would fail for the case of function application: in order to allow recursive functions, the type rule for application is a terminal rule relying on the type given for the function in the program’s signature. However, proving this case requires induction on the statement that the body of the function is well-typed, which is most certainly a type derivation of a longer length (i.e. longer than one step), prohibiting us from using the induction hypothesis. Note in this particular case that the length of the derivation for the evaluation statement does decrease. An induction over the length of the derivation for premise (4.2) alone fails similarly. Consider the last step in the derivation of premise (4.1) being derived by the application of a structural rule, then the length of the derivation for (4.2) remains exactly the same, while the length of the derivation for premise (4.1) does decrease by one step.

Using induction on the lexicographically ordered lengths of the type and evaluation derivations allows us to use the induction hypothesis if either the length of the deriva- tion for premise (4.2) is shortened or if the length of the derivation for premise (4.2) remains unchanged while the length of the typing derivation is reduced. We first treat the cases where the last step in the typing derivation was obtained by application of a structural rule, which are all the cases which leave the length of the derivation for the evaluation unchanged. We then continue to consider the remaining cases based 604.3 Operational Semantics on the evaluation rule that had been applied last to derive premise (4.2), since the remaining type rules are all syntax directed and thus unambiguously determined by the applied evaluation rule.

How can such a "double induction" be performed in Coq?

I tried induction EVAL; induction WELL_TYPED, but got 418 subgoals, most of wich are unprovable.

I also tried to start with induction EVAL and use induction WELL_TYPED later, but go stucked in a similar situation.

Yves Yves · Accepted Answer · 2017-10-12T07:18:16

I agree with @jbapple that a minimal example is better. That said, it may be that you are simply missing a concept of length of derivation. Note that the usual concept of proof by induction over a predicate actually implements something that is close to induction over the height of derivations, but not quite.

I propose that you exhibit two new predicates eval_n and has_type_n that each express the same as eval and has_type, but with an extra argument with meaning "... and derivation has size n". There are several ways in which size might be defined but I suspect that height will be enough for you.

Then you can prove

eval a1 .. ak <-> exists n, eval_n a1 .. ak n

and

has_type a1 .. ak <-> exists n, has_type a1 .. ak n

You should then be able to prove

forall p : nat * nat, forall a1 ... ak, eval_n a1 .. ak (fst p) ->
   has_type_n a1 .. ak (snd p) -> YOUR GOAL

by well founded induction on pairs of natural numbers, using the lexical order construction of library Wellfounded (I suggest library Lexicographic_Product.v, it is a bit of an overkill for just pairs of natural numbers, but you only need to find the right instantiation).

This will be unwieldy because induction hypotheses will only refer to pairs of numbers that are comparable for the lexical order, and you will have to perform inversions on the hypotheses concerning eval_n and has_type_n, but that should go through.

There probably exists a simpler solution, but for lack of more information from your side, I can only propose the big gun.

How to perform induction over two inductive predicates?

1 Answers