Simultaneous generalisation

Stream: general

[Jannis Limperg]

I need a tactic that works like generalize, but for multiple terms at once. Does this already exist?

Background: Generalising over multiple terms at once is not the same thing as generalising one after the other. Consider the following (slightly contrived) example:

universes u

inductive Vec (α : Sort u) : ℕ → Sort (max 1 u)
| nil : Vec 0
| cons {n} : α → Vec n → Vec (n + 1)

namespace Vec

inductive eq {α} : ∀ n m, Vec α n → Vec α m → Prop
| nil : eq 0 0 nil nil
| cons {n m} {xs : Vec α n} {ys : Vec α m} {x y : α} :
  x = y →
  eq n m xs ys →
  eq (n + 1) (m + 1) (cons x xs) (cons y ys)

end Vec

example {α : Sort u} {x y n m} {xs : Vec α n} {ys : Vec α m}
  : Vec.eq (n + 1) (m + 1) (Vec.cons x xs) (Vec.cons y ys)
  → Vec.eq n m xs ys :=
begin
  intro h,
  -- generalize eq : n + 1 = i₁,         -- The `n + 1`         in h is not generalised.
  -- generalize eq : Vec.cons x xs = i₁, -- The `Vec.cons x xs` in h is not generalised.
  refine
    (λ (i₁ i₂ : ℕ) (i₃ : Vec α i₁) (i₄ : Vec α i₂)
      (i₁_eq : i₁ = n + 1) (i₂_eq : i₂ = m + 1) (i₃_eq : i₃ == Vec.cons x xs)
      (i₄_eq : i₄ == Vec.cons y ys) (h' : Vec.eq i₁ i₂ i₃ i₄),
      (_ : Vec.eq n m xs ys))
    (n + 1) (m + 1) (Vec.cons x xs) (Vec.cons y ys) rfl rfl heq.rfl heq.rfl h,
  -- This is the state I want after generalising `n + 1`, `m + 1`, `Vec.cons x xs` and `Vec.cons y ys`.
   cases h; assumption
end

The individual generalisations can't be performed because the resulting term would not be type-correct -- but when we generalise everything at once, it works out.

[Simon Hudon]

have you tried generalize_hyp?

[Jannis Limperg]

Ah yes, sorry, generalize only works on the target. I've fixed the example, but the problem remains.

[Simon Hudon]

There's also h_generalize for issues arising with heterogeneous types / equality but you might want to take a step back and make the types in your theorem less dependent. For instance, you might want to define a function from vector to list, reason about list equality and reflect that equality back into a statement about vectors

[Jannis Limperg]

I've looked into h_generalize, but it doesn't seem applicable to this particular problem.

The generalisation step is supposed to be part of a larger tactic and I'd like to support use cases like this, even if it may be wiser to reduce the amount of dependency. (Also, this issue originally came up in a more realistic example, so it's not entirely academic.) Seems like I'll have to just write the tactic.

[Mario Carneiro]

Umm... isn't the proof here just intro h, cases h, assumption?

[Jannis Limperg]

Yes, that's the 'contrived' part of the example. ;)

[Mario Carneiro]

When I have more nontrivial variants on generalize I just write out the suffices term manually

[Mario Carneiro]

usually this is before an induction and I find I want to make other changes to the state as well, such that straight double generalize wouldn't cut it

[Mario Carneiro]

Plus, the description of the problem here is more or less guaranteed to create heq terms

[Mario Carneiro]

If you want just generalize : a = x and not generalize e : a = x then it is easier

[Mario Carneiro]

which is probably the right approach in these situations anyway

[Mario Carneiro]

Do you have a more realistic example? You can also use match to perform multiple generalizes like this but it probably also requires the target type

[Jannis Limperg]

No, I need the equations. This is indeed for a smarter induction tactic which properly generalises over compound index arguments (basically McBride's "Elimination with a Motive" tactic). The heqs often aren't an issue because they will be eliminated, or at least turned into homogeneous equations, after the fact. The example is realistic if you pretend that cases doesn't already exist: induction should be a generalisation of cases.

[Mario Carneiro]

well you can always get the equations with a multiple generalize, you know

[Mario Carneiro]

it's just one more dependent arg

[Mario Carneiro]

The heqs often aren't an issue because they will be eliminated, or at least turned into homogeneous equations, after the fact

What's confusing me about this example is that I would be fighting to turn the goal after the tactic into the one before the tactic

[Mario Carneiro]

induction should be a generalisation of cases

The generalizes done in cases are generally bad for induction, because they limit the inductive hypothesis too much and usually make it useless

[Mario Carneiro]

Do you have an example where this better induction tactic would be useful and cases / induction fail?

[Jannis Limperg]

My induction is essentially a reimplementation of Coq's dependent induction and should be broadly equivalent to Agda's pattern matching, Coq's Equations plugin and Lean's equation compiler, so it's not exactly a radical new idea. Here's an example from Jasmin's course (which motivates the whole project):

def state :=
string → ℕ

def state.update (name : string) (val : ℕ) (s : state) : state :=
λname', if name' = name then val else s name'

notation s `{` name ` ↦ ` val `}` := state.update name val s

inductive stmt : Type
| skip   : stmt
| assign : string → (state → ℕ) → stmt
| seq    : stmt → stmt → stmt
| ite    : (state → Prop) → stmt → stmt → stmt
| while  : (state → Prop) → stmt → stmt

inductive big_step : stmt × state → state → Prop
| skip {s} :
  big_step (skip, s) s
| assign {x a s} :
  big_step (assign x a, s) (s{x ↦ a s})
| seq {S T s t u} (hS : big_step (S, s) t)
    (hT : big_step (T, t) u) :
  big_step (seq S T, s) u
| ite_true {b : state → Prop} {S T s t} (hcond : b s)
    (hbody : big_step (S, s) t) :
  big_step (ite b S T, s) t
| ite_false {b : state → Prop} {S T s t} (hcond : ¬ b s)
    (hbody : big_step (T, s) t) :
  big_step (ite b S T, s) t
| while_true {b : state → Prop} {S s t u} (hcond : b s)
    (hbody : big_step (S, s) t)
    (hrest : big_step (while b S, t) u) :
  big_step (while b S, s) u
| while_false {b : state → Prop} {S s} (hcond : ¬ b s) :
  big_step (while b S, s) s

infix ` ⟹ `:110 := big_step

lemma not_big_step_while_true {S s t} :
  ¬ (while (λ_, true) S, s) ⟹ t :=
begin
  intro hw,
  induction' hw,
  case while_true {
    exact ih_hw_1
  },
  case while_false {
    apply hcond,
    trivial
  }
end

cases wouldn't suffice here; the proof requires induction. Regular induction leaves us with an unprovable while_false case because the naive generalisation it performs throws information away. So you have to know how to generalise the goal yourself; my induction' does this for you. It also recognises that most of the cases are impossible and solves them automatically.

Now, this example doesn't have the dependencies between index argument that are the topic of this thread. But having hopefully established the utility of induction', the only question is whether it should randomly fail on perfectly good hypotheses because I was too lazy to implement a more general procedure for simultaneous generalisation. That would seem unfortunate to me.

[Mario Carneiro]

Right, this is the sort of thing I don't think you can get right in general

[Mario Carneiro]

picking the right induction hypothesis is a very difficult problem. You may have a heuristic that works for this problem but then it fails for a different use case. In this case you need to know that the left arg is a while true but if s was a more specific thing like \lam _, 0 then you might accidentally hold that fixed as well and then it wouldn't be provable

[Mario Carneiro]

I believe that induction has the correct default behavior, and it is best to have the user manually use generalize to indicate what they want to hold fixed in the induction hypothesis

[Jannis Limperg]

I'm not claiming that this tactic can intuit the correct level of generality for every lemma. But in my experience, it is usually right if you state the lemma at the right level of generality. And I should stress again that I'm doing more or less exactly what the equation compiler is doing:

meta def not_big_step_while_true' : ∀ {S s t}, (while (λ_, true) S, s) ⟹ t → false
| S s u (@while_true b _ _ t _ hcond hbody hrest) := not_big_step_while_true' hrest
| _ _ _ (while_false hcond) := hcond trivial

(The termination checker complains for whatever reason, hence the meta.) If every modern dependently typed language employs this strategy, it's probably a decent strategy.

[Mario Carneiro]

The termination checker complains because the equation compiler actually failed in this example!

[Mario Carneiro]

It fell back on well founded recursion which has pretty bad error messages

[Mario Carneiro]

If you are replicating the equation compiler in lean, that's a big project (that I encourage). But I would suggest a principled approach to it rather than chaining tactics because this is more likely to create brittleness and edge cases (some of which exist already in induction, cases, and the equation compiler)

[Jannis Limperg]

Mario Carneiro said:

The termination checker complains because the equation compiler actually failed in this example!

I see. That's a problem with the equation compiler though; Agda would have no issue with this definition.

Mario Carneiro said:

If you are replicating the equation compiler in lean, that's a big project (that I encourage). But I would suggest a principled approach to it rather than chaining tactics because this is more likely to create brittleness and edge cases (some of which exist already in induction, cases, and the equation compiler)

That's fair. My goal is much more modest: an induction tactic that can handle Jasmin's course contents with minimal ceremony.

[Mario Carneiro]

FWIW the way I write proofs of theorems like your example is:

lemma not_big_step_while_true {S s t} :
  ¬ (while (λ_, true) S, s) ⟹ t :=
begin
  generalize e : (while (λ_, true) S, s) = c,
  intro hw,
  induction hw generalizing s; cases e,
  { exact hw_ih_hrest rfl },
  { apply hw_hcond,
    trivial }
end

[Mario Carneiro]

Unfortunately this throws away the case tags so you can't use case, and propagate_tags doesn't work because of the unique rename problem

[Mario Carneiro]

I see. That's a problem with the equation compiler though; Agda would have no issue with this definition.

Do you know how Agda's equation compiler works? It is the most complex equation compiler I am aware of, and because the things it does are axiomatic it has a lot of leeway to just do things and not worry about the reason behind them

[Mario Carneiro]

But from my point of view there is a very real issue that explains why induction and cases use different inductive hypotheses

[Mario Carneiro]

One thing that's not clear to me about induction' is how you decide what to generalize

[Mario Carneiro]

In order for that theorem to be provable you need to generalize at least s, as well as some S' that is equal to (while (λ_, true) S, s)

[Mario Carneiro]

If you are thinking to just generalize everything, that will limit its usefulness when this is an induction buried inside a larger proof. Or are you expecting that induction' should always be the first tactic in the proof, and the goal state is already curated for consumption?

[Jannis Limperg]

Mario Carneiro said:

FWIW the way I write proofs of theorems like your example is: [...]

Yeah, that's exactly what the tactic does as well. Generalise indices, induction, eliminate the equations for the generalised indices, simplify the induction hypothesis.

with_cases preserves the case tags:

lemma not_big_step_while_true {S s t} :
  ¬ (while (λ_, true) S, s) ⟹ t :=
begin
  generalize e : (while (λ_, true) S, s) = c,
  intro hw,
  with_cases { induction hw generalizing s; cases e },
  case while_true {
    exact hw_ih_hrest rfl
  },
  case while_false {
    apply hw_hcond,
    trivial
  }
end

Mario Carneiro said:

Do you know how Agda's equation compiler works? It is the most complex equation compiler I am aware of, and because the things it does are axiomatic it has a lot of leeway to just do things and not worry about the reason behind them

Not in any detail. I know that it translates the patterns to case trees, but not to eliminators. Termination checking is a separate pass based on a 'size-change' criterion, but I don't actually know what that is. If I wanted to build an equation compiler, I'd start with Jesper Cockx's paper on proof-relevant unification. Matthieu Sozeau probably also has a paper on the Equations plugin.

Mario Carneiro said:

One thing that's not clear to me about induction' is how you decide what to generalize

It generalises every compound index argument of the hypothesis we eliminate ('eliminee'), here (while (λ_, true) S, s). It then reverts every hypothesis that doesn't occur in the eliminee to get the most general induction hypothesis. (This can be overridden with a 'fixing' clause akin to induction's 'generalizing'.)

There is currently no way to prevent compound index arguments from being generalised, though I could add a flag to that effect. I would indeed assume that most uses of induction are near the top of the proof. This is certainly the case for the boring programming languages proofs where this tactic will be most useful. For induction within a longer proof, I would tend to use a lemma or assert.

[Mario Carneiro]

another common pattern in boring PL proofs is induction h1; cases h2; cases equality

[Mario Carneiro]

for example in proving determinism with a small step semantics

[Mario Carneiro]

or big step for that matter

[Jannis Limperg]

PR: #2982