## Stream: maths

### Topic: More examples about logic reasoning

#### mindwarelab (Apr 26 2019 at 19:08):

Hello, it would be possible to have some basic tautology by examples? I found extremely hard to reconciliate, my knowledge about rules of inference into actual code. Thanks

#### mindwarelab (Apr 26 2019 at 19:15):

Thanks for replying to me so quickly. Yes, I have taken a look and I have currently open, but, I found it extremely hard to reconcile how to do it with what I know anyway. It is far from anything I ever programmed with. A simple, modus pones p and (p->q)->q, seems so complex. (that's a bit my feedback as not used to this kind of proof technologies.)

#### Johan Commelin (Apr 26 2019 at 19:17):

@mindwarelab I don't understand exactly what kind of examples you are looking for. Also, experience has showed this community that it depends very much on your background how we should help you. Are you a mathematician or a computer scientist?

#### Johan Commelin (Apr 26 2019 at 19:18):

Do you want:

lemma tautology (X : Type) (x : X) : x = x := rfl


#### mindwarelab (Apr 26 2019 at 19:21):

I am a Bsc. computer science, so my approach is more C style approach to the problems, but I understand this is more a mathematician tool.

I am trying to write the rule of inference of modus pones as I do on paper, so extract the premises and then arrive at a conclusion.

#### Johan Commelin (Apr 26 2019 at 19:22):

Just post some code, we'll give feedback

#### Kevin Buzzard (Apr 26 2019 at 19:22):

Are these examples http://wwwf.imperial.ac.uk/~buzzard/xena/html/source/M1F_introduction/prop_exercises.html of any use?

#### Johan Commelin (Apr 26 2019 at 19:23):

Weren't those written by a mathematician, for mathematicians? :grinning:

#### Kevin Buzzard (Apr 26 2019 at 19:23):

Right. And Theorem Proving In Lean was written by computer scientists for computer scientists.

#### Kevin Buzzard (Apr 26 2019 at 19:24):

So somehow those are the two options available.

Fair enough

#### mindwarelab (Apr 26 2019 at 19:24):

Just post some code, we'll give feedback

theorem prop_1 : A ∧ (A → B) → B := sorry
in pseudo code i would write premise1 = A, premise2 = A->B, conclusion = B I am struggluing to chope down some actual LEAN code.

#### Johan Commelin (Apr 26 2019 at 19:24):

@mindwarelab have you had a course on functional programming (Haskell and such)?

#### Johan Commelin (Apr 26 2019 at 19:25):

@mindwarelab Use

lean
code goes here



#### mindwarelab (Apr 26 2019 at 19:25):

mindwarelab have you had a course on functional programming (Haskell and such)?

No, I have never approach any of them, I will have a classe the next year. I honestly know nothing about.

#### Patrick Massot (Apr 26 2019 at 19:25):

Did you actually try to read anything from the links I posted?

#### mindwarelab (Apr 26 2019 at 19:26):

Right. And Theorem Proving In Lean was written by computer scientists for computer scientists.

Thanks, I will take a look rn :)

#### Patrick Massot (Apr 26 2019 at 19:26):

Because the questions you ask is more than covered there

#### Johan Commelin (Apr 26 2019 at 19:26):

theorem prop_1 : A ∧ (A → B) → B :=
begin
intro h,
cases h with a f,
apply f,
exact a
end


#### Johan Commelin (Apr 26 2019 at 19:26):

I didn't test that code

#### Patrick Massot (Apr 26 2019 at 19:27):

It's pretty safe...

#### mindwarelab (Apr 26 2019 at 19:27):

Because the questions you ask is more than covered there

I know it's there, but I find extremely hard to extrapolate it from the documentation itself. I am kind of used to other type of documentation and for me it's very challenging. But again I really have to do it, so yeas I will read it over and over.

#### mindwarelab (Apr 26 2019 at 19:28):

Imperial college https://wwwf.imperial.ac.uk/~buzzard/xena/html/source/M1F_introduction/prop_exercises.html is pretty good! Thanks!

#### Kevin Buzzard (Apr 26 2019 at 19:30):

you are doing the wrong degree ;-)

#### mindwarelab (Apr 26 2019 at 19:30):

theorem prop_1 : A ∧ (A → B) → B :=
begin
intro h,
cases h with a f,
apply f,
exact a
end


Thanks a lot, I will try it.
I need to go to do the exercises, but thanks for the suggestions!

#### mindwarelab (Apr 26 2019 at 19:32):

you are doing the wrong degree ;-)

Ahaha well ... this is for another conversation :D

#### Neil Strickland (Apr 29 2019 at 12:31):

Here are some other versions that also work.

lemma taut_a (A B : Prop) : A ∧ (A → B) → B :=
begin
rintro ⟨ha,hab⟩,
exact hab ha
end

lemma taut_b (A B : Prop) : A ∧ (A → B) → B
| ⟨ha,hab⟩ := hab ha

lemma taut_c (A B : Prop) : A ∧ (A → B) → B := λ ⟨ha,hab⟩, hab ha

lemma taut_d (A B : Prop) : A ∧ (A → B) → B :=  λ h, h.2 h.1


Last updated: May 09 2021 at 10:11 UTC