CODEWITHSUNDEEP
coqproof
Necto
Necto

Reputation: 2654

How to prove functions equal, knowing their bodies are equal?

How can we prove the following?:

Lemma forfun: forall (A B : nat->nat), (forall x:nat, A x = B x) ->
                                       (fun x => A x) = (fun x => B x).
Proof.

Upvotes: 5

Views: 1571

Answers (1)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23592

The principle you want is known as functional extensionality; in its most general form, it says

Axiom fun_ext : forall (A B : Type) (f g : A -> B),
  (forall x : A, f x = g x) -> f = g.

Unfortunately, in spite of being useful, this principle is independent of Coq's base logic, which means that it is not possible to prove it or refute it. However, Coq's logic was designed so that it would be safe to assume this principle as an axiom in the theory, and Coq's standard library already has that principle defined so that you can use it.

Upvotes: 3

Related Questions