and

Stream: new members

[Thomas Laraia]

How do you take two hypotheses and combine them into one with an ∧?

[Thomas Laraia]

And taking the other approach, is there a reason the have does not work in the last line?

example (a b : ℕ) : a ∣ b ↔ gcd a b = a :=
begin
  split,
  intro h,
  have j := dvd_refl a,
  apply dvd_antisymm,
  have d := dvd_gcd_iff a b a,
end

[Kevin Buzzard]

Thomas Laraia said:

How do you take two hypotheses and combine them into one with an ∧?

You can use the constructor for and, which is called and.intro, or you can just use the pointy brackets "general constructor for a structure" construction:

example (P Q : Prop) (hP : P) (hQ : Q) : P ∧ Q :=
and.intro hP hQ

example (P Q : Prop) (hP : P) (hQ : Q) : P ∧ Q := ⟨hP, hQ⟩

[Patrick Massot]

Thomas, it will be easier to help you if you provide more context. You should read #mwe. It happens that I recognized an exercise from my tutorials, so I can help you anyway, but it would easier to say so, with a precise reference to the exercise (they are numbered precisely for this purpose).

[Patrick Massot]

Note also that you don't need the answer to this question to do the exercise (but you'll need to know at some point of course).

[Patrick Massot]

Let's move to your second question now, the have error.

[Patrick Massot]

Reading error messages is tricky but very important. The error message says:

function expected at
  dvd_gcd_iff
term has type
  ?m_1 ∣ ?m_2.gcd ?m_3 ↔ ?m_1 ∣ ?m_2 ∧ ?m_1 ∣ ?m_3

[Patrick Massot]

Lean expect a function here because you ask it to apply dvd_gcd_iffto a, b and a.

[Patrick Massot]

While dvd_gcd_iff is not a function (here function is meant in the dependent type theory sense, which includes a proof of a forall or imply statement), it's an equivalence.

[Patrick Massot]

It's an equivalence between statements that feature mysterious ?m_1, ?m_2, ?m_3. It means those are implicit arguments that Lean will try to infer automatically. This is nice from Lean, but the downside is it won't let you provide those arguments explicitly unless you really insist.

[Patrick Massot]

You can check all this by writing #check dvd_gcd_iff above the exercise.

[Patrick Massot]

This indeed doesn't show the argument. So you can ask Lean to see them anyway with #check @dvd_gcd_iff

[Patrick Massot]

Note the curly braces around the argument in the answer (and also when this lemma is explained before the exercise). This is what marks arguments as implicit.

[Patrick Massot]

This @ trick saying "I want to provide all arguments, please don't try to help" also works inside proofs, so you can fix your last line by using @dvd_gcd_iff there as well. Needless to say, this is not the expected solution. You don't need to know any of this at this stage, but it will become necessary at some point.

[Patrick Massot]

For something which is half way between the expected solution and your idea, you can try: have d : a ∣ a.gcd b ↔ a ∣ a ∧ a ∣ b := dvd_gcd_iff,. This is give you a proof script that is easier to read and will use the fact that those implicit arguments can be inferred from the statement.

[Thomas Laraia]

@Patrick Massot Perfect, thank you for the detailed explanation and for linking the minimal working examples page, I'll make sure I do this in the future.