Zulip Chat Archive
Stream: general
Topic: Proof-irrelevance issue?
Xavier Martinet (Nov 25 2021 at 15:11):
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 (Nov 25 2021 at 15:15):
Hint: if you put triple #backticks around the lines containing code, it will appear nicely formatted. (Single backticks work for inline text.)
Anne Baanen (Nov 25 2021 at 15:16):
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 (Nov 25 2021 at 15:18):
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 (Nov 25 2021 at 15:19):
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 (Nov 25 2021 at 15:47):
Thanks a lot @Anne Baanen ! indeed it is due to def lem
vs lemma lem
And thanks for the explanation :)
Last updated: Dec 20 2023 at 11:08 UTC