rewriting in dependent expressions

Stream: new members

[Scott Buckley]

import Mathlib.Data.Vector.Basic
lemma foo (fnA : (n m k : Nat) → (n = m + k) → Vector Nat n)
          (fnB : (n : Nat) → Vector Nat n) (a b : Nat):
    fnA (a + (b + 1)) a (b + 1) (by omega) = fnB (a + (b + 1)) →
    fnA (a.succ + b)  a (b + 1) (by omega) = fnB (a.succ + b) := by
intros h1
have h2 : (a + (b + 1)) = (a.succ + b) := by omega
-- here I am unable to do any rewriting with h2, nor can I generalize
-- the relevant expressions.
grind -- but grind works

In the above MWE, I have an equality where the type of the expressions are dependent on some of the subterms. There are also some other dependencies in the expression you can see. I have an equality that theoretically could let me rewrite some subterms, thus allowing me to use my assumption, but doing so non-universally would break the type-correctness of the expressions. grind will get the job done, but I have been unable to extract any useful information about how it's getting it done, and nevertheless I am more interested in how this might be solved without grind.

In such a circumstance, do you have any tips for how to proceed in this proof? Are there any clever dependent rewriting tricks? I could go viaHeq and cast I think, although I'm not sure this would necessarily help, as the LHS and RHS of this equality each would break with non-global rewrites.

A way I found to solve this problem was to write a similar lemma, where the complex terms in question were reduced to a single variable, which then allowed me to perform a "global rewrite" by performing case destruction on a given equality, as in the following example. It seems that I should be able to get to a similar state in the foo proof via generalizing, but generalizing also couldn't cope with the dependencies.

import Mathlib.Data.Vector.Basic
lemma foo_aux (fnA : (n m k : Nat) → (n = m + k) → Vector Nat n)
          (fnB : (n : Nat) → Vector Nat n) (a b x y : Nat)
          (inv1 : x = a + b) (inv2 : y = a + b):
    x = y →
    fnA x a b inv1 = fnB x →
    fnA y a b inv2 = fnB y := by
intros hxy h
-- rw [← hxy] -- does not work
cases hxy
exact h

(side note: conv seems to skip over the dependent term a + (b + 1), presumably because it is used in a type dependency. It would be lovely to have a version of conv that allowed rewriting in dependent terms, but carried around the consequences of these rewrites to enforce that other subterms were appropriately rewritten. I suppose this would mean that the entire conv system would need to allow for types to change recursively, and I can see this being non-trivial. Further, propositions depending on these terms would potentially need to be re-proven, although if we are only replacing equal terms then perhaps this isn't a problem.)

[Yan Yablonovskiy 🇺🇦]

If you are okay with Mathlib tactics you can do:

import Mathlib.Data.Vector.Basic
import Mathlib.Tactic

lemma foo_aux (fnA : (n m k : Nat) → (n = m + k) → Vector Nat n)
          (fnB : (n : Nat) → Vector Nat n) (a b x y : Nat)
          (inv1 : x = a + b) (inv2 : y = a + b):
    x = y →
    fnA x a b inv1 = fnB x →
    fnA y a b inv2 = fnB y := by
intros hxy h
rw! [← hxy] -- works
cases hxy
exact h

which is like a 'dependent' rewrite

[Scott Buckley]

Beautiful! I did a bunch of googling about "dependent rewriting" for Lean, but never came across this. I have seen ! versions of a few tactics used here and there - is it a pattern that this refers to versions of the tactics supporting more dependency? I should read more thoroughly through the documentation for mathlib's tactics.

Thank you for the insanely fast response!

[Ruben Van de Velde]

"!" means "try harder" in some way - in contrapose! or by_contra! it means "push the negation inwards", for example

[Scott Buckley]

Yeah, this makes sense, thank you.

While we're on the topic, I'm finding that I'm unable to perform rw! [foo] at h in my original environment, although I haven't been able to recreate the issue in my MWE. It looks like a very similar to the below:

import Mathlib.Data.Vector.Basic
import Mathlib.Tactic

lemma foo_aux (fnA : (n m k : Nat) → (n = m + k) → Vector Nat n)
          (fnB : (n : Nat) → Vector Nat n) (a b x y : Nat)
          (inv1 : x = a + b) (inv2 : y = a + b):
    x = y →
    fnA x a b inv1 = fnB x →
    fnA y a b inv2 = fnB y := by
intros hxy h
rw! [hxy] at h -- here is where the issue occurs
cases hxy
exact h

I get the following error, in a context where I can't see any reason the rewrite shouldn't work - it's almost identical to in the MWE.

unknown free variable `_fvar.18510`

Does this ring any bells already? I'm just checking because it might be a fair bit of work to get a MWE exhibiting the same behaviour.

[Aaron Liu]

Yes, I fixed that bug recently

[Aaron Liu]

as a workaround you can do rewrite! instead of rw!

[Scott Buckley]

@Aaron Liu that did the trick! Thanks :)

[Aaron Liu]

the fix was merged 2 days ago (#33686) so it should also be fine if you bump mathlib