inductive proposition tactics

Stream: new members

[Billy Price]

Is there a tactic for proving inductively defined propositions, where the right constructor to apply is always obvious because they're all mutually exclusive in their conclusions? I find myself having to apply many constructors of the inductive proposition, all of which terminate to some atomic constructor, or can be solved with assumption.

[Kevin Buzzard]

Is tauto of any use?

[Kevin Buzzard]

It uses solve_by_elim

[Mario Carneiro]

That sounds like constructor

[Mario Carneiro]

which is basically the same as apply T.constr1 <|> apply T.constr2 <|> ...

[Billy Price]

tauto didn't work, and constructor works as expected for 1 step, so I did repeat {constructor} and that solved it - but this will only work if the proposition reduces to atomic constructors, not if one of the goals produced is part of the context (for which assumption would work). I'm guessing I could do something like repeat {constructor <|> assumption} - but is that the cleanest way to proceed?

Here's a contrived example to illustrate this

inductive WF : context → type → term → Prop
| star {Γ}         : WF Γ Unit ⁎
| top  {Γ}         : WF Γ Ω ⊤
| bot  {Γ}         : WF Γ Ω ⊥
| and  {Γ p q}     : WF Γ Ω p → WF Γ Ω q → WF Γ Ω (p ⋀ q)
| or   {Γ p q}     : WF Γ Ω p → WF Γ Ω q → WF Γ Ω (p ⋁ q)
| imp  {Γ p q}     : WF Γ Ω p → WF Γ Ω q → WF Γ Ω (p ⟹ q)
| elem {Γ A a α}   : WF Γ A a → WF Γ (𝒫 A) α → WF Γ Ω (a ∈ α)
| pair {Γ A B a b} : WF Γ A a → WF Γ B b → WF Γ (A ×× B) ⟪a,b⟫
| var  {Γ A n}     : list.nth Γ n = some A → WF Γ A (var n)
| comp {Γ A φ}     : WF (A::Γ) Ω φ → WF Γ (𝒫 A) ⟦φ⟧
| all  {Γ A φ}     : WF (A::Γ) Ω φ → WF Γ Ω (∀' φ)
| ex   {Γ A φ}     : WF (A::Γ) Ω φ → WF Γ Ω (∃' φ)

example : WF [] Ω p → WF [] Ω q → WF [] Ω (p ⋀ q) :=
begin
  intros h₁ h₂,
  constructor,
  assumption,
  assumption
end

[Johan Commelin]

Does tidy do it for you?

[Billy Price]

Nope, no progress

[Mario Carneiro]

it seems you have a proof already. Do you have a better example?

[Mario Carneiro]

also that's not an #mwe

[Mario Carneiro]

probably constructor; assumption will work on this and similar goals

[Mario Carneiro]

so something like induction h; constructor; assumption will take care of most of your theorem

[Mario Carneiro]

@Billy Price

[Billy Price]

Here's an example of how this problem blows up, which is only half done because of the definition of biimp. Essentially I want a tactic which will do as much of this as it can by itself, and then leave me with the non-trivial goals (in this case those can be solved by assumption - but I can imagine more general usage where I'd need to do more work).

import tactic.tidy
import tactic.tauto

inductive type : Type
| Unit | Omega | Prod (A B : type)| Pow (A : type)

notation `Ω` := type.Omega
def Unit := type.Unit
infix `××`:max := type.Prod
notation `𝒫`A :max := type.Pow A

def context := list type

inductive term : Type
| star : term
| top  : term
| bot  : term
| and  : term → term → term
| or   : term → term → term
| imp  : term → term → term
| elem : term → term → term
| pair : term → term → term
| var  : ℕ → term
| comp : term → term
| all  : term → term
| ex   : term → term

-- * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
-- Notation and derived operators
-- * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *

notation `𝟘` := term.var 0
notation `𝟙` := term.var 1
notation `𝟚` := term.var 2
notation `𝟛` := term.var 3
notation `𝟜` := term.var 4
notation `𝟝` := term.var 5

notation `⁎` := term.star    -- input \asterisk
notation `⊤` := term.top     --       \top
notation `⊥` := term.bot     -- input \bot
infixr ` ⟹ `:60 := term.imp -- input \==>
infixr ` ⋀ ` :70 := term.and -- input \And or \bigwedge
infixr ` ⋁ ` :59 := term.or  -- input \Or or \bigvee


def biimp (p q: term) := (p ⟹ q) ⋀ (q ⟹ p)
infix ` ⇔ `:60 := biimp -- input \<=>

infix ∈ := term.elem
notation `⟦` φ `⟧` := term.comp φ

notation `⟪` a `,` b `⟫` := term.pair a b

prefix `∀'`:1 := term.all
prefix `∃'`:2 := term.ex

def lib_eq (a₁ a₂ : term) : term := ∀' (a₁ ∈ 𝟘) ⇔ (a₂ ∈ 𝟘)
infix ` ≃ ` :50 := lib_eq


-- * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
open term



inductive WF : context → type → term → Prop
| star {Γ}         : WF Γ Unit ⁎
| top  {Γ}         : WF Γ Ω ⊤
| bot  {Γ}         : WF Γ Ω ⊥
| and  {Γ p q}     : WF Γ Ω p → WF Γ Ω q → WF Γ Ω (p ⋀ q)
| or   {Γ p q}     : WF Γ Ω p → WF Γ Ω q → WF Γ Ω (p ⋁ q)
| imp  {Γ p q}     : WF Γ Ω p → WF Γ Ω q → WF Γ Ω (p ⟹ q)
| elem {Γ A a α}   : WF Γ A a → WF Γ (𝒫 A) α → WF Γ Ω (a ∈ α)
| pair {Γ A B a b} : WF Γ A a → WF Γ B b → WF Γ (A ×× B) ⟪a,b⟫
| var  {Γ A n}     : list.nth Γ n = some A → WF Γ A (var n)
| comp {Γ A φ}     : WF (A::Γ) Ω φ → WF Γ (𝒫 A) ⟦φ⟧
| all  {Γ A φ}     : WF (A::Γ) Ω φ → WF Γ Ω (∀' φ)
| ex   {Γ A φ}     : WF (A::Γ) Ω φ → WF Γ Ω (∃' φ)

variables p q r : term

example : WF [Unit,Ω] Ω p → WF [Unit,Ω] Ω q  → WF [Unit,Ω] Ω r  → WF [Unit,Ω] Ω ((p ⋀ 𝟙) ⇔ ((q ⋀ r ⋀ 𝟙) ⟹ ((⁎ ≃ 𝟙) ⋀ p))) :=
begin
  intros,
  constructor,
  constructor,
  constructor,
  assumption,
  constructor,
  simp,
  constructor,
  constructor,
  assumption,
  constructor,
  assumption,
  constructor,
  simp,
  constructor,
  constructor,
  constructor,
  constructor,
  constructor,
  constructor,
  constructor,
  simp,
  constructor,
  constructor,
  simp,
  constructor,
  simp,
  constructor,
  constructor,
  constructor,
  simp,
  constructor,
  simp,
  constructor,
  constructor,
  constructor,
  simp,
  assumption,
  sorry
end

[Billy Price]

Btw some of my Unicode notation is non-obvious. I'm using \And, \Or, \==>, \<=>, \asterisk to name a few relevant ones. Also the numbers are \b0, \b1, \b2, etc.

[Mario Carneiro]

Off topic, but your WF.all rule looks wrong. The argument A is not fixed by application, so you are allowed to assume any type for it

[Mario Carneiro]

Your definition of lib_eq is also wrong, you have to lift a1 and a2

[Mario Carneiro]

the theorem itself is false, because ⁎ ≃ 𝟙 isn't well typed

[Mario Carneiro]

Modulo those things, this proof works:

theorem WF.biimp {Γ p q} (h1 : WF Γ Ω p) (h2 : WF Γ Ω q) : WF Γ Ω (p ⇔ q) :=
WF.and (WF.imp h1 h2) (WF.imp h2 h1)

theorem WF.lib_eq {Γ A a b} (h1 : WF Γ A a) (h2 : WF Γ A b) : WF Γ Ω (a ≃ b) := sorry

example (hp : WF [Unit,Ω] Ω p) (hq : WF [Unit,Ω] Ω q) (hr : WF [Unit,Ω] Ω r) :
  WF [Unit,Ω] Ω ((p ⋀ 𝟙) ⇔ ((q ⋀ r ⋀ 𝟙) ⟹ ((⁎ ≃ 𝟘) ⋀ p))) :=
by apply_rules [WF.biimp, WF.and, WF.imp, WF.lib_eq, WF.star, WF.var]; refl

[Mario Carneiro]

Hm, the proof works without WF.biimp in the list, but it is twice as long. I think there should be a reducibility setting in apply_rules so that it doesn't go unfold-happy

[Mario Carneiro]

local attribute [irreducible] biimp

works, of course

[Billy Price]

Mario Carneiro said:

Off topic, but your WF.all rule looks wrong. The argument A is not fixed by application, so you are allowed to assume any type for it

Isn't it fixed by the hypothesis that \phi is well-formed in the context with A put at the start?

Mario Carneiro said:

Your definition of lib_eq is also wrong, you have to lift a1 and a2

Good point, didn't think about lifting it here, I was just making do by manually lifting the variables, which is why I wrote ⁎ ≃ 𝟙, instead of ⁎ ≃ 𝟘 - isn't that well formed?

[Mario Carneiro]

Isn't it fixed by the hypothesis that \phi is well-formed in the context with A put at the start?

The problem is that the term doesn't record what A is, so you can have multiple types for one term. It's not exactly broken, I think they call this "implicit typing" and it was used by Curry I think for lambda terms, but in the modern tradition the terms carry enough typing information so that the context uniquely determines the type of the expression

[Mario Carneiro]

Good point, didn't think about lifting it here, I was just making do by manually lifting the variables, which is why I wrote ⁎ ≃ 𝟙, instead of ⁎ ≃ 𝟘 - isn't that well formed?

Oh I see, you made = a binder. Well that's one way to solve the problem :shrug:

[Billy Price]

Can you explain the role of the semicolon? I was under the impression it's just a new-line-separator, but it seems that there's a lot of cleanup done after apply_rules, whereas if I do this in tactic mode, I have 20 goals to apply refl to.

[Kevin Buzzard]

semicolon means "apply next tactic to all goals generated by this tactic"

[Mario Carneiro]

As an example of the bad behavior of implicit typing here, ∃' ∀' (𝟘 ≃ 𝟙) (or with your binding equals operator, ∃' ∀' (𝟙 ≃ 𝟚)) is well typed of type Ω but assuming that you can prove that Unit is a singleton and 𝒫 Unit is not, this term is both provably true and provably false and hence the system is inconsistent

[Mario Carneiro]

The problem is that the term is vague about what type is being asserted to be a singleton

[Mario Carneiro]

There are only 3 goals produced by apply_rules in my test, which are kicked back from the var rule

[Mario Carneiro]

a less golfed version is

begin
  apply_rules [WF.biimp, WF.and, WF.imp, WF.lib_eq, WF.star, WF.var],
  all_goals {refl}
end

[Billy Price]

Mario Carneiro said:

As an example of the bad behavior of implicit typing here, ∃' ∀' (𝟘 ≃ 𝟙) (or with your binding equals operator, ∃' ∀' (𝟙 ≃ 𝟚)) is well typed of type Ω but assuming that you can prove that Unit is a singleton and 𝒫 Unit is not, this term is both provably true and provably false and hence the system is inconsistent

Thanks for that explanation, I forget when or why I dropped the type parameter from term.all and term.ex. Thanks for pointing that out

[Mario Carneiro]

I recall you had a lot more types before (on things like application) and I think I pointed out that they were not necessary

[Mario Carneiro]

The place where you need types are when you are introducing a new type variable that can't be inferred from the arguments

[Billy Price]

Yeah I must have taken that too far haha

[Billy Price]

R.e. apply_rules, can I be lazy with it and tell it to try all of the rules? Like everything starting with WF.?

[Mario Carneiro]

I think there is a way to make sets of rules for it

[Mario Carneiro]

the apply_rules documentation has an example

[Kevin Buzzard]

tactic#apply_rules

[Billy Price]

Mario Carneiro said:

The place where you need types are when you are introducing a new type variable that can't be inferred from the arguments

Does this mean that term.comp doesn't need an explicit type parameter, because the WF constructor | comp {Γ A φ} : WF (A::Γ) Ω φ → WF Γ (𝒫 A) term.comp φ tells you the type of the variable free in phi?

[Billy Price]

To be honest I don't quite understand what exact kind of situation you are referring to in "when you are introducing a new type variable". Is this strictly just when defining WF?

[Mario Carneiro]

No, I think comp needs a type

[Mario Carneiro]

An easy rule is anything with a binder (where the hypothesis to the WF rule has an extended context) needs a type

[Mario Carneiro]

The general form of the claim would be that any term p has at most one type given a context Gamma

[Mario Carneiro]

and I think you can even claim at most one type derivation

[Billy Price]

That's very eye opening thank you. I was just here thinking "my terms seem so freely defined - but my proof constraints are enough to allow you to only prove true statements when you choose appropriate types for each term"

[Billy Price]

If I have more related questions I'll continue them back in my usual channel/topic. I just thought my original question was general enough.

[Mario Carneiro]

the problem is that the terms are responsible for carrying type assignments from one line of proof to the next, so if they are too free then you can interpret the same term in two incompatible ways during the same proof

[Mario Carneiro]

proofs are irrelevant but terms aren't

[Billy Price]

@Mario Carneiro I've just noticed that my elem : term -> term -> term constructor doesn't have a type in the contstructor. It's WF rule does not extend the context, yet a term like 0 \in 1 doesn't tell me the types of 0 or 1 (though I can't think of an example term that's true with one type and false with another). Why is this different?

I noticed this because for all other term constructors I have a corresponding lemma which extracts a well-formedness proof of each argument, but I can't write one that does WF Γ Ω (a∈α) → WF Γ A a, because I can't presume to know A. This tempts me to add a type to the elem constructor - but is there a reason I shouldn't?