left-hand-side depends on right-hand-side

Stream: general

[Hunter Freyer]

Can anyone explain what "cases tactic failed, when eliminating equality left-hand-side depends on right-hand-side" means?

[Hunter Freyer]

I'd provide an example but it's deep in some complex stuff, and I don't understand it well enough to produce a more minimal example

[Floris van Doorn]

Here is a minimal example:

example (n m : ℕ) (h : m + m = n) : true := by { cases h, trivial } -- works
example (n m : ℕ) (h : n + m = n) : true := by { cases h, trivial } -- error

cases h can be used on equalities when either the left-hand side or the right-hand side is a variable in the local context. If you do that, the variable is removed from the context and every occurrence of it is replaced by the other side of the equality. Now in the second example above, the variable n also occurs on the left-hand side of the equality, so after you replace all n by n + m you still cannot remove n from the context. If that happens, the tactic raises an error. So the problem is that the left-hand side contains the variable you want to remove.

[Floris van Doorn]

Note: sometimes doing dsimp before cases simplifies the equality so that the variable doesn't occur in the left hand side anymore.

[Hunter Freyer]

The thing is that there aren't any equalities in my context

[Hunter Freyer]

I'm trying to do cases on a variable of a dependent type, so maybe there's like, hidden implicit equalities

[Floris van Doorn]

What tactic did you execute to get this error? If you did cases what is the type of the variable you cased on?

[Floris van Doorn]

Is it an inductive type? An inductive family of types? Are all indices variables? If so, you can try induction instead.
(If you don't know what this means, the question is probably "no")

[Hunter Freyer]

aight, here's my code in all it's newbtacular glory: https://pastebin.com/jjMR45t8

[Hunter Freyer]

I'm modeling reduction rules over a kind of primitive recursive functions

[Hunter Freyer]

Line 55 is the source of the error. Bizzarely, vscode isn't letting me copy-paste the error itself

[Floris van Doorn]

I think the problem is that you have an inductive family of types with 2 explicit indices, and that the variable f_g occurs in both of them.

[Hunter Freyer]

huh, okay. Moving the subst that set the two to be equal into the specific case where I'm using it has at least made the error go away.

[Floris van Doorn]

If you replace the offending tactic with

            generalize eq1 : f_f.comp f_g = c1,
            generalize eq2 : g_f.comp f_g = c2,
            intro h2,
            cases h2,
            subst eq2,

You see that you cannot now substitute eq1 away, since neither side is a variable. This is roughly what cases is doing under the hood.

[Floris van Doorn]

Sorry, replace intro h2, cases h2 with the above snippet.

[Floris van Doorn]

So

instance step_decidable :
    Π (tin tout) (f: fn tin tout) (g: fn tin tout),
    decidable (step f g) :=
begin
    intros,
    induction f,
    case comp {
        cases g,
        case comp {
            by_cases (f_tint = g_tint),
            focus {
                subst h,
                by_cases (f_g = g_g),
                focus {
                    subst h,
                    cases f_ih_f g_f,
                    case is_true {
                        apply (is_true),
                        constructor,
                        assumption,
                        done
                    },
                },
            },
            apply(is_false),
            generalize eq1 : f_f.comp f_g = c1,
            generalize eq2 : g_f.comp f_g = c2,
            intro h2,
            cases h2,
            subst eq2,
        },
    }
end

[Hunter Freyer]

incidentally, when I have a goal which is effectively <empty type> -> false, is there a less verbose way of solving that than to introduce and do cases on the empty type?

[Floris van Doorn]

If the empty type is sufficiently simple you can do rintro ⟨⟩

[Hunter Freyer]

hmm, do I need to import something to use that?

[Floris van Doorn]

rintro is a nice tactic to introduce variables and immediately case on them. You need to import tactic.basic for it.

[Floris van Doorn]

(and have mathlib)

[Hunter Freyer]

I'll look into that

[Hunter Freyer]

actually, I have a more general question here... the constructors of step have two forms: ones where they literally spell out the shape of the type parameters, and ones where they essentially require congruence mod step (e.g., comp_f)

[Hunter Freyer]

I'm trying to show it's decidable. The algorithm is essentially, "find a constructor that matches the value. If that constructor requires analogous parts of the parallel structure to be related by step, call it recursively"

[Hunter Freyer]

and the tactics I'm writing seem... excessive for the simplicity of that algorithm

[Hunter Freyer]

(oh: and of course, if there's no constructor that matches, demonstrate that in is_false)

[Hunter Freyer]

Is there a better way than doing this kind of case analysis on the arguments to the relation? Is there some way of going more from the constructors of step to say, "whatever this value is, if I can unify it with one of the constructors, then yes, the type is inhabited"?

[Floris van Doorn]

Probably you can pretty easily write a tactic that deals with all the easy cases for you (and with more effort a tactic that proves the decidability itself). AFAIK we don't have a tactic that does this off-the-shelf.

[Floris van Doorn]

For example,

instance step_decidable :
    Π (tin tout) (f: fn tin tout) (g: fn tin tout),
    decidable (step f g) :=
begin
    intros,
    induction f; cases g,
end

gives 40 goals, and this solves 32 of them:

instance step_decidable :
    Π (tin tout) (f: fn tin tout) (g: fn tin tout),
    decidable (step f g) :=
begin
    intros,
    induction f; cases g; try { left, rintro ⟨⟩, done }; try { right, constructor, done },
end

[Floris van Doorn]

(if you don't have mathlib, you can replace the rintro by intro h, cases h)

[Hunter Freyer]

nice! I had something like this, but that's nicer

[Hunter Freyer]

I'm still really struggling with this. I'm trying to prove that the "step" relation is antireflexive, but any time I try to work with \not (step f f) [i.e., try to do induction on it], I get this error

[Hunter Freyer]

Here's my code:

@[derive decidable_eq]
inductive val : Type
| nat
| nil
| cons : Π (car : val) (cdr: val), val

@[derive decidable_eq]
inductive fn : val -> val -> Type
| zero : fn val.nil val.nat
| succ : fn val.nat val.nat
| car  : Π {tcar tcdr: val}, fn (val.cons tcar tcdr) tcar
| cdr  : Π {tcar tcdr: val}, fn (val.cons tcar tcdr) tcdr
| nil  : Π {tin : val}, fn tin val.nil
| cons : Π {tin tcar tcdr: val} (car : fn tin tcar) (cdr: fn tin tcdr), fn tin (val.cons tcar tcdr)
| comp : Π {tin tint tout: val} (f : fn tint tout) (g: fn tin tint), fn tin tout
| prec : Π {trest tout: val} (z_case : fn trest tout) (s_case: fn (val.cons val.nat (val.cons tout trest)) tout),
    fn (val.cons val.nat trest) tout

inductive step : Π {tin tout} (f: fn tin tout) (g: fn tin tout), Prop
| proj_car : Π {tin tcar tcdr} {car:fn tin tcar} {cdr: fn tin tcdr},
    step (fn.comp fn.car (fn.cons car cdr)) car
| proj_cdr : Π {tin tcar tcdr} {car:fn tin tcar} {cdr: fn tin tcdr},
    step (fn.comp fn.cdr (fn.cons car cdr)) cdr
| comp_f : Π {tin tint tout} {f1 f2:fn tint tout} {g: fn tin tint}
    (_ : step f1 f2),
    step (fn.comp f1 g) (fn.comp f2 g)

def step_antireflex {tin tout} (f: fn tin tout) : ¬ (step f f) :=
begin
    sorry
end```

[Hunter Freyer]

A specific example:

def step_antireflex {tin tout} (f: fn tin tout) : ¬ (step f f) :=
begin
    intros,
    intro h,
    induction h,
end

[Hunter Freyer]

... gives "induction tactic failed, argument #3 of major premise type step f f is an index, but it occurs more than once"

[Mario Carneiro]

In order to do induction, you have to first generalize the indices so that they are distinct, with separate constraints

[Mario Carneiro]

theorem step_antireflex {tin tout} (f: fn tin tout) : ¬ (step f f) :=
begin
  suffices : ∀ g, f = g → ¬ step f g,
  { exact this _ rfl },
  intros g e h,
  induction h,
  iterate 2 {
    have := congr_arg (fn.sizeof _ _) e,
    simp [fn.sizeof, λ a b, show sizeof = fn.sizeof a b, from rfl] at this,
    linarith },
  { cases e, cases h_ih rfl }
end