diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
commit | 9043add656177eeac1491a73d2f3ab92bec0013c (patch) | |
tree | 2b0092c84bfbf718eca10c81f60b2640dc8cab05 /test-suite/bugs/closed/8004.v | |
parent | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff) |
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'test-suite/bugs/closed/8004.v')
-rw-r--r-- | test-suite/bugs/closed/8004.v | 47 |
1 files changed, 47 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/8004.v b/test-suite/bugs/closed/8004.v new file mode 100644 index 00000000..81863999 --- /dev/null +++ b/test-suite/bugs/closed/8004.v @@ -0,0 +1,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. + +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. |