# Zulip Chat Archive

## 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

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

@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):

#### 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