## 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.

(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 04 2023 at 23:01 UTC