1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
|
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2025 -- Inria - CNRS - Paris-Saclay University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(********************************************************************)
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require HighOrd.
Require Import ClassicalEpsilon.
Lemma function_extensionality:
forall A B (f g : A -> B),
(forall x, f x = g x) -> f = g.
Admitted.
(* Why3 assumption *)
Definition infix_eqeq {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}
(m1:a -> b) (m2:a -> b) : Prop :=
forall (x:a), ((m1 x) = (m2 x)).
Notation "x == y" := (infix_eqeq x y) (at level 70, no associativity).
(* Why3 goal *)
Lemma extensionality {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b} :
forall (m1:a -> b) (m2:a -> b), infix_eqeq m1 m2 -> (m1 = m2).
Proof.
intros m1 m2 h1.
apply function_extensionality.
intros x.
generalize (h1 x).
easy.
Qed.
|
