Instantly share code, notes, and snippets.

# mathink/setoid_advent_2014.v Last active Aug 29, 2015

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.