Andres Erbsen andres-erbsen
andres-erbsen
/ funext_from_interval.v
Created
November 1, 2018 23:02
— forked from JasonGross/funext_from_interval.v
A derivation of function extensionality from the interval in Coq using private inductives
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Module Import Interval. | |
| Unset Elimination Schemes. | |
| (** An [interval] is the quotient of [bool] under the trivial | |
| relation, that [true = false]. Based on the real interval, we | |
| call the left endpoint [zero], the right endpoint [one], and the | |
| proof of equality [seg : zero = one]. *) | |
| Private Inductive interval := zero | one. | |
| Axiom seg : zero = one. | |
| (** The eliminator for the interval says that if you send [zero] |