constructor choose wrong constructor

Stream: new members

[Horatiu Cheval]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Scott Morrison]

You should try out solve_by_elim.