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
42
43
44
45
46
47
|
Require Export Coq.Program.Tactics Coq.Classes.SetoidTactics Coq.Classes.CMorphisms .
Set Universe Polymorphism.
Delimit Scope category_theory_scope with category_theory.
Open Scope category_theory_scope.
Infix "∧" := prod (at level 80, right associativity) : category_theory_scope.
Class Setoid A := {
equiv : crelation A;
setoid_equiv :: Equivalence equiv
}.
Notation "f ≈ g" := (equiv f g) (at level 79) : category_theory_scope.
Open Scope list_scope.
Generalizable All Variables.
Fixpoint list_equiv `{Setoid A} (xs ys : list A) : Type :=
match xs, ys with
| nil, nil => True
| x :: xs, y :: ys => x ≈ y ∧ list_equiv xs ys
| _, _ => False
end.
Axiom proof_admitted : False.
Tactic Notation "admit" := abstract case proof_admitted.
#[export] Program Instance list_equivalence `{Setoid A} : Equivalence list_equiv.
Next Obligation.
repeat intro.
induction x; simpl; split; auto.
reflexivity.
Qed.
Next Obligation.
repeat intro.
generalize dependent y.
induction x, y; simpl; intros; auto.
destruct X; split.
now symmetry.
intuition.
Qed.
Next Obligation.
admit.
Defined.
|
