Stream: general

Topic: Simultaneous generalisation

Jannis Limperg (Jun 02 2020 at 16:04):

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 (Jun 02 2020 at 16:16):

have you tried generalize_hyp?

Jannis Limperg (Jun 02 2020 at 16:29):

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

Simon Hudon (Jun 02 2020 at 16:40):

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 (Jun 02 2020 at 17:02):

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 (Jun 02 2020 at 17:10):

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

Jannis Limperg (Jun 02 2020 at 17:10):

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

Mario Carneiro (Jun 02 2020 at 17:11):

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

Mario Carneiro (Jun 02 2020 at 17:12):

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 (Jun 02 2020 at 17:12):

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

Mario Carneiro (Jun 02 2020 at 17:13):

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

Mario Carneiro (Jun 02 2020 at 17:13):

which is probably the right approach in these situations anyway

Mario Carneiro (Jun 02 2020 at 17:16):

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 (Jun 02 2020 at 17:17):

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 (Jun 02 2020 at 17:19):

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

Mario Carneiro (Jun 02 2020 at 17:19):

it's just one more dependent arg

Mario Carneiro (Jun 02 2020 at 17:20):

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 (Jun 02 2020 at 17:22):

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 (Jun 02 2020 at 17:34):

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

Jannis Limperg (Jun 03 2020 at 01:04):

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 (Jun 03 2020 at 01:06):

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

Mario Carneiro (Jun 03 2020 at 01:09):

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 (Jun 03 2020 at 01:10):

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 (Jun 03 2020 at 01:30):

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 (Jun 03 2020 at 01:51):

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

Mario Carneiro (Jun 03 2020 at 01:51):

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

Mario Carneiro (Jun 03 2020 at 01:57):

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 (Jun 03 2020 at 02:05):

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 (Jun 03 2020 at 02:09):

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 (Jun 03 2020 at 02:11):

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 (Jun 03 2020 at 02:13):

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 (Jun 03 2020 at 02:15):

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

Mario Carneiro (Jun 03 2020 at 02:16):

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

Mario Carneiro (Jun 03 2020 at 02:16):

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 (Jun 03 2020 at 02:18):

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 (Jun 03 2020 at 02:33):

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 (Jun 03 2020 at 02:38):

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

Mario Carneiro (Jun 03 2020 at 02:38):

for example in proving determinism with a small step semantics

Mario Carneiro (Jun 03 2020 at 02:38):

or big step for that matter

Jannis Limperg (Jun 08 2020 at 02:14):

PR: #2982

Last updated: May 13 2021 at 17:42 UTC