Proof-irrelevance issue?

Stream: general

[Xavier Martinet]

Hi,

I am a bit confused by Lean's behavior here. I have a theorem:

`
variables p q : Prop

theorem mytheorem (hp : p) (hq : q) : p ∧ q ∧ p :=
begin
apply and.intro,
exact hp,
apply and.intro,
exact hq,
exact hp
end
`

It can also be built in forward, like this:

`
variables p q : Prop

theorem mytheorem_fwd (hp : p) (hq : q) : p → q ∧ p → p ∧ q ∧ p := @and.intro p (and q p)
`

but if I want to create a lemma whose proof term is and q p and replace it in the my_theorem proof term, it is not working:

`
variables p q : Prop

lemma lem : Prop → Prop → Prop := and
lemma failed_mytheorem : p → q ∧ p → p ∧ q ∧ p := @and.intro p (lem q p)
`

The following message is displayed:

type mismatch, term and.intro has type p → lem q p → p ∧ lem q p but is expected to have type p → q ∧ p → p ∧ q ∧ p

I suspect that the fact that the type q ∧ p is different from lem (while having the exact same proof terms!) is related to proof irrelevance.
Am I missing something? Is there a way to create lemmas in the Sort universe without creating new types?

[Anne Baanen]

Hint: if you put triple #backticks around the lines containing code, it will appear nicely formatted. (Single backticks work for inline text.)

[Anne Baanen]

Probably the issue is that you define lem as lemma lem instead of def lem: lemma instructs Lean to forget the details of the definition, and only remember the type.

[Anne Baanen]

This is not quite the same as proof irrelevance: q ∧ p and lem q p are elements of Prop, which is a Type, so they are not considered irrelevant. The elements of q ∧ p and lem q p are all considered equivalent though.

[Anne Baanen]

In other words, proof irrelevance states if x y : p and p : Prop, then x = y. This is different from the rule if p q : Prop then p = q (which would be contradictory!).

[Xavier Martinet]

Thanks a lot @Anne Baanen ! indeed it is due to def lem vs lemma lem
And thanks for the explanation :)