Zulip Chat Archive

Stream: general

Topic: left-hand-side depends on right-hand-side


Hunter Freyer (Sep 23 2020 at 01:35):

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

Hunter Freyer (Sep 23 2020 at 01:36):

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 (Sep 23 2020 at 01:46):

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 (Sep 23 2020 at 01:47):

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

Hunter Freyer (Sep 23 2020 at 01:48):

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

Hunter Freyer (Sep 23 2020 at 01:48):

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

Floris van Doorn (Sep 23 2020 at 01:49):

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 (Sep 23 2020 at 01:50):

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 (Sep 23 2020 at 01:51):

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

Hunter Freyer (Sep 23 2020 at 01:51):

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

Hunter Freyer (Sep 23 2020 at 01:52):

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

Floris van Doorn (Sep 23 2020 at 01:53):

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 (Sep 23 2020 at 01:55):

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 (Sep 23 2020 at 01:55):

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 (Sep 23 2020 at 01:56):

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

Floris van Doorn (Sep 23 2020 at 01:56):

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 (Sep 23 2020 at 01:57):

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 (Sep 23 2020 at 01:59):

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

Hunter Freyer (Sep 23 2020 at 02:00):

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

Floris van Doorn (Sep 23 2020 at 02:00):

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

Floris van Doorn (Sep 23 2020 at 02:00):

(and have mathlib)

Hunter Freyer (Sep 23 2020 at 02:01):

I'll look into that

Hunter Freyer (Sep 23 2020 at 02:04):

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 (Sep 23 2020 at 02:05):

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 (Sep 23 2020 at 02:05):

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

Hunter Freyer (Sep 23 2020 at 02:06):

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

Hunter Freyer (Sep 23 2020 at 02:08):

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 (Sep 23 2020 at 02:11):

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 (Sep 23 2020 at 02:15):

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

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

Hunter Freyer (Sep 23 2020 at 02:17):

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

Hunter Freyer (Sep 25 2020 at 00:16):

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 (Sep 25 2020 at 00:18):

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 (Sep 25 2020 at 00:20):

A specific example:

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

Hunter Freyer (Sep 25 2020 at 00:21):

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

Mario Carneiro (Sep 25 2020 at 00:56):

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

Mario Carneiro (Sep 25 2020 at 01:02):

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

Last updated: Dec 20 2023 at 11:08 UTC