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
|
Require Import ListDef Morphisms Setoid.
Global Generalizable All Variables.
Class Equiv A := equiv: relation A.
Section ops.
Context (M : Type -> Type).
Class MonadReturn := ret: forall {A}, A -> M A.
End ops.
Arguments ret {M MonadReturn A} _.
Class Monad (M : Type -> Type) `{forall A, Equiv A -> Equiv (M A)}
`{MonadReturn M} : Prop :=
{
mon_ret_proper `{Equiv A} :: Proper (equiv ==> equiv) (@ret _ _ A)
}.
Section S.
Context `{Equivalence A eqA}.
Inductive PermutationA : list A -> list A -> Prop := .
Global Instance: Equivalence PermutationA.
Admitted.
Global Instance PermutationA_cons :
Proper (eqA ==> PermutationA ==> PermutationA) (@cons A).
Admitted.
Lemma foo a l x (IHl : PermutationA (x::l) (l ++ (x :: nil))) : PermutationA (x::a::l) (a::l++(x :: nil)).
Proof.
rewrite <-IHl.
Abort.
End S.
|
