Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
Theorem Prover Advent Calendar day 10.
Set Implicit Arguments.
Unset Strict Implicit.
Require Export Basics Tactics Setoid Morphisms.
Structure Setoid :=
carrier:> Type;
equal: relation carrier;
prf_Setoid:> Equivalence equal
Existing Instance prf_Setoid.
Notation Setoid_of eq := (@Build_Setoid _ eq _).
Print Equivalence.
Print Graph.
Notation "(== :> S )" := (equal (s:=S)).
Notation "(==)" := (== :> _).
Notation "x == y :> S" := (equal (s:=S) x y)
(at level 70, y at next level, no associativity).
Notation "x == y" := (x == y :> _) (at level 70, no associativity).
Program Canonical Structure eq_Setoid (A: Type) := Setoid_of (@eq A).
Check 1 == 1.
Check true == false.
Eval simpl in S == S.
Definition ext_eq (X Y: Type)(f g: X -> Y) :=
forall (x: X), f x = g x.
Arguments ext_eq X Y / f g.
Program Canonical Structure fun_Setoid (X Y: Type): Setoid :=
Setoid_of (@ext_eq X Y).
Next Obligation.
- intros f x; reflexivity.
- intros f g Heq x; rewrite Heq; reflexivity.
- intros f g h Heqfg Heqgh x; rewrite (Heqfg x); apply Heqgh.
Definition plus1 (n: nat): nat := n + 1.
Check (plus1 == S).
Eval simpl in S == S.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment