cases on expressions that evaluate to inductive types

Stream: lean4

[Paige Thomas]

If I have an inductive type, say

inductive Formula_ : Type
  | false_ : Formula_
  | true_ : Formula_
  | atom_ : String → Formula_
  | not_ : Formula_ → Formula_
  | and_ : Formula_ → Formula_ → Formula_
  | or_ : Formula_ → Formula_ → Formula_
  | imp_ : Formula_ → Formula_ → Formula_
  | iff_ : Formula_ → Formula_ → Formula_

and I have an expression e that evaluates to a type Formula_, and a hypothesis h : e = not_ e, is there a tactic that will immediately prove that this is a contradiction? It seems that I need to do something like set F := e before cases h will work.

[Chase Norman]

Canonical can solve this outright, but I've taken the liberty of using induction to handle the absurd cases:

example : e ≠ Formula_.not_ e := by
  -- canonical
  induction e with
  | not_ e a_ih => exact fun a ↦ a_ih (by simpa only [Formula_.not_.injEq] using a)
  | _ => exact fun a ↦ by simpa only [reduceCtorEq] using a

[Paige Thomas]

Hmm. I think maybe I didn't communicate what I meant very well. I can prove that the hypothesis is a contradiction by using set to replace the expression by a single variable name and then uses cases on the hypothesis, I was just wondering why it is necessary to use set first.

[Paige Thomas]

For example, I have the hypothesis contra : replace_atom_all_rec σ phi = replace_atom_all_rec σ phi.not_. If I do set H := replace_atom_all_rec σ phi and then cases contra it solves the goal, but I'm not sure I understand why I need to do the set first and not just use cases contra.

[Edward van de Meent]

you can do this:

example (e : Formula_) (he : e = .not_ e) : False := by
  have : sizeOf e = sizeOf (Formula_.not_ e) := congr(sizeOf $he)
  simp at this

[Edward van de Meent]

the main idea here is that he leads to an infinite regression, however since values of inductives have a definable "size", this would lead to some natural number being its own successor

[Edward van de Meent]

or even a one-liner proof: simpa using congr(sizeOf $he)

[Edward van de Meent]

you do need Mathlib.Tactic for this, specifically the congr quotation

[Robin Arnez]

Use cases he. Under the hood it will do the same thing @Edward van de Meent recommended

[Edward van de Meent]

i was under the impression that OP tried that and it didn't work? but indeed, it looks like that also works...

[Robin Arnez]

Oh I guess the question is rather <complex expression> = .not_ <complex expression> not working?

[Paige Thomas]

Yes, it is that cases h does not work on h: <complex expression> = .not_ <complex expression>. For some reason I have to do something like set F := <complex expression> before cases h.

[Kyle Miller]

docs#Lean.MVarId.acyclic is what is responsible for the way cases handles acyclicity, and in Lean.MVarId.isTarget you can see that it looks specifically for a free variable on one side and that free variable appearing in the other side.

That explains exactly why you need to use set (or generalize) as a first step.

I imagine the reason it was coded this way is that it's assumed that it's only supposed to support constructor applications, so the other reasoning in docs#Lean.Meta.unifyEq? will reduce to the case of a free variable on one side in that case.

I wonder how far dependent elimination could get in more cases if instead of an acyclicity prover it was a general sizeOf-based prover. Then, for example, it might be able to make progress on List.append indexes, etc.

[Paige Thomas]

Hmm. Ok. I might have to come back to trying to understand that in its entirety at a later time. Thank you.