Zulip Chat Archive

Stream: new members

Topic: inductive proposition tactics


view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 09 2020 at 06:42):

Is tauto of any use?

view this post on Zulip Kevin Buzzard (Jun 09 2020 at 06:42):

It uses solve_by_elim

view this post on Zulip Mario Carneiro (Jun 09 2020 at 06:48):

That sounds like constructor

view this post on Zulip Mario Carneiro (Jun 09 2020 at 06:49):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jun 09 2020 at 07:15):

Does tidy do it for you?

view this post on Zulip Billy Price (Jun 09 2020 at 07:19):

Nope, no progress

view this post on Zulip Mario Carneiro (Jun 09 2020 at 07:34):

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

view this post on Zulip Mario Carneiro (Jun 09 2020 at 07:37):

also that's not an #mwe

view this post on Zulip Mario Carneiro (Jun 09 2020 at 07:38):

probably constructor; assumption will work on this and similar goals

view this post on Zulip Mario Carneiro (Jun 09 2020 at 07:39):

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

view this post on Zulip Mario Carneiro (Jun 09 2020 at 07:39):

@Billy Price

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 09 2020 at 09:25):

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

view this post on Zulip Mario Carneiro (Jun 09 2020 at 09:27):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 09 2020 at 09:33):

local attribute [irreducible] biimp

works, of course

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 09 2020 at 09:42):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Billy Price (Jun 09 2020 at 09:50):

Yeah I must have taken that too far haha

view this post on Zulip 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.?

view this post on Zulip Mario Carneiro (Jun 09 2020 at 09:53):

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

view this post on Zulip Mario Carneiro (Jun 09 2020 at 09:54):

the apply_rules documentation has an example

view this post on Zulip Kevin Buzzard (Jun 09 2020 at 09:55):

tactic#apply_rules

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jun 09 2020 at 09:59):

No, I think comp needs a type

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 09 2020 at 10:01):

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

view this post on Zulip 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"

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 09 2020 at 10:06):

proofs are irrelevant but terms aren't

view this post on Zulip 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