# Zulip Chat Archive

## Stream: new members

### Topic: inductive type

#### jachym simon (Apr 29 2020 at 10:40):

Hi!

I am doing some stuff with mathematical logic in Lean and i would like to ask you the following.

I have defined logic formulas as an inductive type with implication and negation (logic atoms are represented by natural numbers) the following way.

```
inductive Form : Type
| p : ℕ → Form
| imp : Form → Form → Form
| neg : Form → Form
```

I would like to somehow express the fact, that some formula B is a sub-formula of some other formula A. That means, that either A = B or that somewhere during the process of creating formula A with the inductive rules, the formula B is used (either in implication or negation (or even as a logical atom) ). Is there some way to express that? Cheers, Jachym

#### Patrick Massot (Apr 29 2020 at 10:41):

This could be an inductively defined Prop

#### Brandon Brown (Apr 30 2020 at 16:20):

How does lean know to prevent lists of heterogeneous types?

e.g.

```
inductive list (α : Type u)
| nil {} : list
| cons : α → list → list
def mylist := (list.cons 2 list.nil)
#check (list.cons bool.true mylist) -- error
```

The `cons`

constructor takes a type `α`

and a `list`

but there is no type specified. I guess I'm not sure why we don't do

`| cons : α → list α → list α`

(which doesn't work)

#### Mario Carneiro (Apr 30 2020 at 16:21):

The type is a parameter, the `(α : Type u)`

on the first line

#### Mario Carneiro (Apr 30 2020 at 16:21):

you are required not to write parameters in the definition of the inductive, they get added in the real type of the constructor

#### Brandon Brown (Apr 30 2020 at 16:22):

Ah I see, yeah

```
#check list.cons -- list.cons : ?M_1 → list ?M_1 → list ?M_1
```

#### Kevin Buzzard (Apr 30 2020 at 17:33):

`#check @list.cons`

is a variant which gets rid of all the random ?'s

#### jachym simon (May 22 2020 at 13:53):

Hello,

I have another question connected to the previous one. I want to create a proposition `equiv`

, that for formulas A B says, that all subformulas are equivalent. Example:

```
inductive Form : Type
| p : ℕ → Form
| imp : Form → Form → Form
| neg : Form → Form
--A = P ⇒ (R ⇒ Q)
--B = P ⇒ (S ⇒ Q)
--equiv A B would be something like (⊢ P ⇔ P) ∧ (⊢ R ⇔ S) ∧ (⊢ Q ⇔ Q)
--("⊢ A" means A is provable, exact definition isnt for my question important (i think... shouldnt be))
example(h1: ⊢ P ⇔ P)(h2: ⊢ R ⇔ S )(h3: ⊢ Q ⇔ Q): equiv (P ⇒ (R ⇒ Q)) (P ⇒ (S ⇒ Q)) := sorry
```

I tried creating a proposition using the Form.rec_on function like this, but it doesnt work. In the first "loop" subparts are determined as `P₁ = P`

, `P₂= (R ⇒ Q)`

. I can show that `⊢ P ⇔ P`

, so what remains is `⊢ (R ⇒ Q) ⇔ (S ⇒ Q)`

. That i cannot show, so it needs to be decomposed further. Now id like the subparts to be `P₁ = R`

and `P₂ = Q`

, but they dont change (which kind of makes sense). Is there some way how to do it?

```
def equiv(P Q:Form): Prop :=
Form.rec_on P
(λ m,
Form.rec_on Q (λ n, ⊢ (p m ⇔ p n))
(λ Q₁ Q₂ q₁ q₂, ⊢ ((p m) ⇔ (Q₁ ⇒ Q₂)))
(λ Q₁ q₁, ⊢ (p m ⇔ ~Q₁)))
(λ P₁ P₂ p₁ p₂,
Form.rec_on Q (λ n, ⊢ ((P₁ ⇒ P₂) ⇔ p n))
(λ Q₁ Q₂ q₁ q₂, (⊢ (P₁ ⇔ Q₁) ∨ (p₂ ∧ q₂)) ∧ (⊢ (P₂ ⇔ Q₂) ∨ (p₁ ∧ q₁)))
(λ Q₁ q₁, ⊢ ((P₁ ⇒ P₂) ⇔ ~Q₁)))
(λ P₁ p₁,
Form.rec_on Q (λ n, ⊢ ((~P₁) ⇔ p n))
(λ Q₁ Q₂ q₁ q₂, ⊢ ((~P₁) ⇔ (Q₁ ⇒ Q₂)) )
(λ Q₁ q₁, ⊢ ((~P₁) ⇔ (~Q₁)) ∨ (p₁ ∧ q₁)))
```

#### Shing Tak Lam (May 22 2020 at 14:13):

#mwe? (emphasis on working)

Why are there `⊢`

s all over the place, is this some custom `notation`

?

#### Jason KY. (May 22 2020 at 14:21):

I think he defined `notation `

⊢` p := provable p`

and I assume `provable`

is defined to be some `Prop`

?

#### Reid Barton (May 22 2020 at 14:21):

I don't understand what `equiv`

is supposed to do. The definition doesn't look that similar to your description.

In any case, I think it would be clearer written using the equation compiler.

#### jachym simon (May 27 2020 at 14:27):

Thanks for the answers. `⊢`

is exactly what Jason writes- a custom notation for a `Prop`

i have defined in my code.

@Reid Barton I didnt exactly know what i am doing with the code hehe. Anyway the thing i wanted was the thing i described and the equation compiler stuff you suggested helped. Thanks

Last updated: May 07 2021 at 00:30 UTC