Stream: new members

Topic: inductive proposition tactics

Billy Price (Jun 09 2020 at 06:40):

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 (Jun 09 2020 at 06:42):

Is tauto of any use?

Kevin Buzzard (Jun 09 2020 at 06:42):

It uses solve_by_elim

Mario Carneiro (Jun 09 2020 at 06:48):

That sounds like constructor

Mario Carneiro (Jun 09 2020 at 06:49):

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

Billy Price (Jun 09 2020 at 07:10):

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 (Jun 09 2020 at 07:15):

Does tidy do it for you?

Billy Price (Jun 09 2020 at 07:19):

Nope, no progress

Mario Carneiro (Jun 09 2020 at 07:34):

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

Mario Carneiro (Jun 09 2020 at 07:37):

also that's not an #mwe

Mario Carneiro (Jun 09 2020 at 07:38):

probably constructor; assumption will work on this and similar goals

Mario Carneiro (Jun 09 2020 at 07:39):

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

@Billy Price

Billy Price (Jun 09 2020 at 09:14):

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 (Jun 09 2020 at 09:17):

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 (Jun 09 2020 at 09:22):

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 (Jun 09 2020 at 09:25):

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

Mario Carneiro (Jun 09 2020 at 09:27):

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

Mario Carneiro (Jun 09 2020 at 09:28):

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 (Jun 09 2020 at 09:33):

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 (Jun 09 2020 at 09:33):

local attribute [irreducible] biimp


works, of course

Billy Price (Jun 09 2020 at 09:33):

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 (Jun 09 2020 at 09:36):

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 (Jun 09 2020 at 09:37):

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 (Jun 09 2020 at 09:42):

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 (Jun 09 2020 at 09:42):

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

Mario Carneiro (Jun 09 2020 at 09:42):

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 (Jun 09 2020 at 09:44):

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

Mario Carneiro (Jun 09 2020 at 09:45):

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

Mario Carneiro (Jun 09 2020 at 09:46):

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 (Jun 09 2020 at 09:48):

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 (Jun 09 2020 at 09:49):

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 (Jun 09 2020 at 09:49):

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 (Jun 09 2020 at 09:50):

Yeah I must have taken that too far haha

Billy Price (Jun 09 2020 at 09:51):

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 (Jun 09 2020 at 09:53):

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

Mario Carneiro (Jun 09 2020 at 09:54):

the apply_rules documentation has an example

Kevin Buzzard (Jun 09 2020 at 09:55):

tactic#apply_rules

Billy Price (Jun 09 2020 at 09:55):

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 (Jun 09 2020 at 09:58):

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 (Jun 09 2020 at 09:59):

No, I think comp needs a type

Mario Carneiro (Jun 09 2020 at 10:00):

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

Mario Carneiro (Jun 09 2020 at 10:01):

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

Mario Carneiro (Jun 09 2020 at 10:01):

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

Billy Price (Jun 09 2020 at 10:04):

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 (Jun 09 2020 at 10:05):

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 (Jun 09 2020 at 10:05):

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 (Jun 09 2020 at 10:06):

proofs are irrelevant but terms aren't

Billy Price (Jul 16 2020 at 11:04):

@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?

Last updated: May 16 2021 at 20:13 UTC