Stream: Coq users

Topic: How to prove that a function is equal to a theorem


view this post on Zulip walker (Mar 01 2022 at 15:32):

From Coq Require Import FunctionalExtensionality.

Inductive LE : nat -> nat -> Prop :=
| le_o (n: nat) : LE O n
| le_nm (n m: nat) (H: LE n m) : LE (S n) (S m).

Fixpoint non_trivial1 (n: nat) : LE n (n + 1) :=
    match n with
    | O => le_o 1
    | S m => le_nm m (m + 1) (non_trivial1 m)
    end.

Theorem non_trivial2: forall n, LE n (n + 1).
Proof.
    intros n.
    induction n; simpl; constructor; auto.
Qed.

Theorem non_trivials_are_equal: non_trivial1 = non_trivial2.
(*function existentialiy does not work here*)

I am doing this solely for playing with Curry-Howard isomorphism purposes.

view this post on Zulip Théo Winterhalter (Mar 01 2022 at 15:36):

Your proof is Qed which means you hide its contents so you can never inspect it.

view this post on Zulip Théo Winterhalter (Mar 01 2022 at 15:37):

If you use Defined instead of Qed your theorem's proof will be transparent and you can hope to prove things about it.

view this post on Zulip walker (Mar 01 2022 at 15:37):

(deleted)

view this post on Zulip walker (Mar 01 2022 at 15:40):

for some reason apply functional_extensionality. fails.

Unable to unify "@Logic.eq (forall _ : ?A, ?B) ?M1348 ?M1349" with
 "@Logic.eq (forall n : nat, LE n (add n 1)) non_trivial1 non_trivial2".

i don't see what the problem is

view this post on Zulip Karl Palmskog (Mar 01 2022 at 15:41):

when you write non_trivial1 = non_trivial2, you are saying that the proofs of each statement are same

view this post on Zulip walker (Mar 01 2022 at 15:41):

I can do forall n, non_trivial1 n = non_trivial2 n. and proof works but I thought functional_extensionality should work

view this post on Zulip Théo Winterhalter (Mar 01 2022 at 15:42):

Maybe it doesn't like that the codomain is Prop as funext is stated with Type?

view this post on Zulip walker (Mar 01 2022 at 15:43):

Yes looks like so But thanks for the Defined trick, now proof works:

Theorem non_trivials_are_equal: forall n, non_trivial1 n = non_trivial2 n.
Proof.
    intros n.
    induction n; auto.
Qed.

view this post on Zulip Théo Winterhalter (Mar 01 2022 at 15:45):

If you want to be proof-relevant I would use Type rather than Prop.

view this post on Zulip Théo Winterhalter (Mar 01 2022 at 15:46):

Also funext is just an axiom so you could also add

Axiom funext_prop :
  forall (A : Type) (P : Prop) (f g : A -> P),
    (forall x, f x = g x) ->
    f = g.

view this post on Zulip walker (Mar 01 2022 at 15:47):

I was wondering perhaps it is not there for a reason, maybe it is not always sound ?

view this post on Zulip Théo Winterhalter (Mar 01 2022 at 15:47):

It's just that in Prop you usually use proof irrelevance directly.

view this post on Zulip walker (Mar 01 2022 at 15:48):

may I ask what does "proof relevance" and "proof irrelevance" mean ? I am not sure I fully understand the concept.

view this post on Zulip Karl Palmskog (Mar 01 2022 at 15:51):

if you have general proof irrelevance, every proof of P : Prop is equal, e.g., if x : P and y : P, then you get x = y with no effort

view this post on Zulip Karl Palmskog (Mar 01 2022 at 15:52):

general proof irrelevance is not the case in Coq without axioms

view this post on Zulip walker (Mar 01 2022 at 16:01):

understood! thanks

view this post on Zulip Gaëtan Gilbert (Mar 01 2022 at 20:24):

walker said:

for some reason apply functional_extensionality. fails.

Unable to unify "@Logic.eq (forall _ : ?A, ?B) ?M1348 ?M1349" with
 "@Logic.eq (forall n : nat, LE n (add n 1)) non_trivial1 non_trivial2".

i don't see what the problem is

probably you need to use functional_extensionality_dep


Last updated: Jan 31 2023 at 12:01 UTC