More examples about logic reasoning

Stream: maths

[mindwarelab]

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

[Patrick Massot]

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

[mindwarelab]

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]

@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]

Do you want:

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

[mindwarelab]

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]

Just post some code, we'll give feedback

[Kevin Buzzard]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

So somehow those are the two options available.

[Johan Commelin]

Fair enough

[mindwarelab]

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]

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

[Johan Commelin]

@mindwarelab Use

```lean
code goes here
```

[mindwarelab]

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]

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

[mindwarelab]

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

Thanks, I will take a look rn :)

[Patrick Massot]

Because the questions you ask is more than covered there

[Johan Commelin]

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

[Johan Commelin]

I didn't test that code

[Patrick Massot]

It's pretty safe...

[mindwarelab]

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]

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

[Kevin Buzzard]

you are doing the wrong degree ;-)

[mindwarelab]

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]

you are doing the wrong degree ;-)

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

[Neil Strickland]

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