Zulip Chat Archive

Stream: maths

Topic: More examples about logic reasoning


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

view this post on Zulip Patrick Massot (Apr 26 2019 at 19:10):

Did you look at https://leanprover.github.io/theorem_proving_in_lean/ and https://leanprover.github.io/logic_and_proof/?

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

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

view this post on Zulip Johan Commelin (Apr 26 2019 at 19:18):

Do you want:

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

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

view this post on Zulip Johan Commelin (Apr 26 2019 at 19:22):

Just post some code, we'll give feedback

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

view this post on Zulip Johan Commelin (Apr 26 2019 at 19:23):

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

view this post on Zulip Kevin Buzzard (Apr 26 2019 at 19:23):

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

view this post on Zulip Kevin Buzzard (Apr 26 2019 at 19:24):

So somehow those are the two options available.

view this post on Zulip Johan Commelin (Apr 26 2019 at 19:24):

Fair enough

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

view this post on Zulip Johan Commelin (Apr 26 2019 at 19:24):

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

view this post on Zulip Johan Commelin (Apr 26 2019 at 19:25):

@mindwarelab Use

```lean
code goes here
```

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

view this post on Zulip Patrick Massot (Apr 26 2019 at 19:25):

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

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

view this post on Zulip Patrick Massot (Apr 26 2019 at 19:26):

Because the questions you ask is more than covered there

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

view this post on Zulip Johan Commelin (Apr 26 2019 at 19:26):

I didn't test that code

view this post on Zulip Patrick Massot (Apr 26 2019 at 19:27):

It's pretty safe...

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

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

view this post on Zulip Kevin Buzzard (Apr 26 2019 at 19:30):

you are doing the wrong degree ;-)

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

view this post on Zulip mindwarelab (Apr 26 2019 at 19:32):

you are doing the wrong degree ;-)

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

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