Zulip Chat Archive

Stream: new members

Topic: inductive type


view this post on Zulip 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

view this post on Zulip Patrick Massot (Apr 29 2020 at 10:41):

This could be an inductively defined Prop

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Apr 30 2020 at 16:21):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 30 2020 at 17:33):

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

view this post on Zulip 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₁)))

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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