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