Stream: Coq users

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

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.

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.

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.

walker (Mar 01 2022 at 15:37):

(deleted)

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

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

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

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?

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.

Théo Winterhalter (Mar 01 2022 at 15:45):

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

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.

walker (Mar 01 2022 at 15:47):

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

Théo Winterhalter (Mar 01 2022 at 15:47):

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

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.

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

Karl Palmskog (Mar 01 2022 at 15:52):

general proof irrelevance is not the case in Coq without axioms

walker (Mar 01 2022 at 16:01):

understood! thanks

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: Oct 13 2024 at 01:02 UTC