inductive type

Stream: new members

[jachym simon]

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]

This could be an inductively defined Prop

[Brandon Brown]

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]

The type is a parameter, the (α : Type u) on the first line

[Mario Carneiro]

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]

Ah I see, yeah

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

[Kevin Buzzard]

#check @list.cons is a variant which gets rid of all the random ?'s

[jachym simon]

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]

#mwe? (emphasis on working)

Why are there ⊢s all over the place, is this some custom notation?

[Jason KY.]

I think he defined notation ⊢ p := provable p and I assume provable is defined to be some Prop?

[Reid Barton]

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]

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