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