Zulip Chat Archive

Stream: new members

Topic: constructor choose wrong constructor


Horatiu Cheval (Mar 27 2021 at 17:05):

I have a type with several constructors. I am doing a proof by induction and most cases can be solved by exact some constructor with a different constructor in each case. However the constructor tactic doesn't work to close the goals because in each case there is some other constructor that advances the goal, but without closing it, and constructor seems to choose that one. How can I make constructor choose the constructor that finishes the proof, instead of the advancing but not finishing one? (it works if I move that universally applicable constructor to the end of the inductive definition, but this doesn't sound like a generalizable technique)

Horatiu Cheval (Mar 27 2021 at 17:06):

import tactic

inductive preformula
| falsum : preformula
| implication : preformula  preformula  preformula
| disjunction : preformula  preformula  preformula
| conjunction : preformula  preformula  preformula

open preformula

infixr `⟹` : 50 := implication
infix `⋀` : 50 := conjunction
infix `⋁` : 50 := disjunction

inductive derivable (Γ : list preformula) : preformula  Type
| Premise {A} : A  Γ  derivable A
| ContrConj {A} : derivable $ A   A  A
| ContrDisj {A} : derivable $ A  A  A

infix `⊢` : 20 := derivable

example {Γ Δ : list preformula} {A : preformula} (h : Γ  Δ) : (Γ  A)  (Δ  A) :=
begin
  intros der,
  induction der,
  case ContrConj{
    constructor,
    -- exact derivable.ContrConj closes the goal
    -- but constructor chooses the Premise constructor
  }
end

Horatiu Cheval (Mar 27 2021 at 17:06):

And constructor works if I switch the order in the definition to put Premise last:

inductive derivable (Γ : list preformula) : preformula  Type
| ContrConj {A} : derivable $ A  A  A
| ContrDisj {A} : derivable $ A   A  A
| Premise {A} : A  Γ  derivable A

Kevin Buzzard (Mar 27 2021 at 17:08):

I was going to say "just do exact [the right constructor]" but this is not the answer you want? The constructor tactic just uses the first constructor which works. Maybe you should write a little tactic of your own here? It would be a neat exercise! See the tutorial.

Horatiu Cheval (Mar 27 2021 at 17:10):

I don't really want to "exact right constructor" because the real proofs have around 20 cases like this

Kevin Buzzard (Mar 27 2021 at 17:10):

See also Chapter 8 of Programming in Lean, they go through the assumption tactic which is of a similar nature (although I cannot guarantee that the code in that pdf still runs, Lean makes no attempt to be backwards compatible right now)

Horatiu Cheval (Mar 27 2021 at 17:11):

Yeah, I was going to learn some tactic writing at some point, so I guess it might be a good moment

Kevin Buzzard (Mar 27 2021 at 17:13):

I'm certainly no tactic expert; the tactic you want might already exist, but I don't know it if it does (what does fconstructor do?). You can probably get away with some combinators (I guess it's possible to say "does this close the goal? If so, do it, else does this close the goal? If so, do it, else..." without too much trouble, but I have extremely limited tactic writing experience, maybe someone else will chime in).

Kevin Buzzard (Mar 27 2021 at 17:14):

Oh -- the other references I know for tactic writing are mentioned at the top of the tutorial (Rob's videos, HHG etc).

Scott Morrison (Mar 28 2021 at 00:29):

You should try out solve_by_elim.


Last updated: Dec 20 2023 at 11:08 UTC