Create a gist now

Instantly share code, notes, and snippets.

Embed
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.
split.
- intros f x; reflexivity.
- intros f g Heq x; rewrite Heq; reflexivity.
- intros f g h Heqfg Heqgh x; rewrite (Heqfg x); apply Heqgh.
Qed.
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