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