So I'm trying to learn lean but I'm struggling with somethin

Stream: new members

[Mimo]

"example (C D S: Prop) (h : C ∧ D → S) : C → D → S := by" this is one of the challenges in the lean intro to logic game and I can't seem to find the answer and there are no hints

[Julian Berman]

Welcome. (#backticks is a good link to have a quick look at).

For your question -- intro c d seems like a good first step. Does this at all help?

[Zhang Qinchuan]

It would be better if you ask question with #mwe using #backticks .

A possible solution for your question:

example (C D S: Prop) (h : C ∧ D → S) : C → D → S := by
intro hc hd
apply h
exact ⟨hc, hd⟩

[Julian Berman]

A further hint is

A further hint without straight giving the answer

Now you're left needing to simply pass c and d into h and you have your proof of S.

well never mind :)

[Mimo]

Julian Berman said:

Welcome. (#backticks is a good link to have a quick look at).

For your question -- intro c d seems like a good first step. Does this at all help?

My first attempt was this

  intro hD```
which I think does the same thing right? But I wasn't sure where to go from there

[Julian Berman]

If you just do intro hD you'll have hD : C, and a goal of D \to S -- meaning you have a proof of C (confusingly named hD) and you need to give a proof that D implies S, but when you see arrows in goals usually that means you need another intro -- intro hc hd will intro twice at once, so now you have hc : C and hd : D, i.e. a proof of C and a proof of D.

[Mimo]

I see. Then what's left is to prove S which I do by applying h, but then the next goal is to prove C \and D (the reciprocate?) but when I try exact hC hD it doesn't work

[Julian Berman]

What's your background, are you a programmer, mathematician, other? (Just to know how best to explain an answer.)

[Mimo]

I'm a first year computer science major. I have basic knowledge of predicate and propositional logic but I'm still struggling to understand tactics a little bit.

[Julian Berman]

OK -- so maybe this helps (if not we can try another way) -- C \to D \to S is a function which eats 2 arguments -- you are supposed to give me a proof of C and a second argument which is a proof of D, and then you get a proof of S.

C \and D \to S on the other hand is not a function of 2 arguments, it's a function of one argument -- the type of that one argument is supposed to be a proof of C \and D simultaneously, which in lean is a term of type And.

[Julian Berman]

These two are of course logically equivalent, which this exercise is trying to make you realize (or at least realize in one direction)

[Julian Berman]

But basically now you need to know Lean syntax for "if I have a thing of type C and a thing of type D how do I get a thing of type C \and D"? And hC hD isn't it, that'd be calling the function hC with one argument but hC is not a function! It's a term of type C.

[Julian Berman]

So the "raw" answer is exact And.intro hC hD -- that's like And's constructor, it gives you a term of type And given 2 terms of the 2 parts of the And

[Julian Berman]

The more "usual" way to get such a term is what Zhang showed, which is exact \<hC, hD\> where that funny bracket syntax is called "anonymous structure literals" -- basically that's a way of getting the same term, but works in more cases than just constructing terms of type And (it works whenever you're trying to get a term of some structure and Lean already knows what type it should be -- but it's easier to just say you'll figure out when to use that when you see it a few times)

[Mimo]

Ah I understand now. But hiw does that prove C \to D \to S ? By transitivity?

[Ruben Van de Velde]

I'm not sure what you mean by "transitivity" here

[Ruben Van de Velde]

You're tasked to prove S, assuming that

1. if C and D are both true, S is also true
2. C is true
3. D is true

[Ruben Van de Velde]

If you want to be very pedantic, there's two more steps here:

4. "C and D" is true (this is the "introduction rule for 'and'")
5. by assumption 1 and 4, S is true (this is the "elimination rule for implication")

[Mimo]

Ruben Van de Velde said:

You're tasked to prove S, assuming that

1. if C and D are both true, S is also true
2. C is true
3. D is true

To be more precise, this is the exercise. I wanted to try doing it without the restrictions first to understand the logic.
image.png
image.png