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

Your proof is `Qed`

which means you hide its contents so you can never inspect it.

If you use `Defined`

instead of `Qed`

your theorem's proof will be transparent and you can hope to prove things about it.

(deleted)

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

when you write `non_trivial1 = non_trivial2`

, you are saying that the *proofs* of each statement are same

I can do `forall n, non_trivial1 n = non_trivial2 n`

. and proof works but I thought functional_extensionality should work

Maybe it doesn't like that the codomain is `Prop`

as funext is stated with `Type`

?

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

If you want to be proof-relevant I would use `Type`

rather than `Prop`

.

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

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

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

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

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

general proof irrelevance is not the case in Coq without axioms

understood! thanks

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: Jun 14 2024 at 17:02 UTC