Commit d566b5f1 authored by Robbert Krebbers's avatar Robbert Krebbers

Curried Permutation_cons instance.

This seems to shorten type class search.
parent 5026b74d
...@@ -27,6 +27,7 @@ Instance: Params (@drop) 1. ...@@ -27,6 +27,7 @@ Instance: Params (@drop) 1.
Arguments Permutation {_} _ _. Arguments Permutation {_} _ _.
Arguments Forall_cons {_} _ _ _ _ _. Arguments Forall_cons {_} _ _ _ _ _.
Remove Hints Permutation_cons : typeclass_instances.
Notation "(::)" := cons (only parsing) : C_scope. Notation "(::)" := cons (only parsing) : C_scope.
Notation "( x ::)" := (cons x) (only parsing) : C_scope. Notation "( x ::)" := (cons x) (only parsing) : C_scope.
...@@ -1331,7 +1332,10 @@ Definition Permutation_skip := @perm_skip A. ...@@ -1331,7 +1332,10 @@ Definition Permutation_skip := @perm_skip A.
Definition Permutation_swap := @perm_swap A. Definition Permutation_swap := @perm_swap A.
Definition Permutation_singleton_inj := @Permutation_length_1 A. Definition Permutation_singleton_inj := @Permutation_length_1 A.
Global Instance Permutation_cons : Proper (() ==> ()) (@cons A x).
Proof. by constructor. Qed.
Global Existing Instance Permutation_app'. Global Existing Instance Permutation_app'.
Global Instance: Proper (() ==> (=)) (@length A). Global Instance: Proper (() ==> (=)) (@length A).
Proof. induction 1; simpl; auto with lia. Qed. Proof. induction 1; simpl; auto with lia. Qed.
Global Instance: Comm () (@app A). Global Instance: Comm () (@app A).
...@@ -1348,9 +1352,7 @@ Proof. ...@@ -1348,9 +1352,7 @@ Proof.
intros. by apply IH, (inj (x ::)). intros. by apply IH, (inj (x ::)).
Qed. Qed.
Global Instance: k : list A, Inj () () (++ k). Global Instance: k : list A, Inj () () (++ k).
Proof. Proof. intros k l1 l2. rewrite !(comm (++) _ k). by apply (inj (k ++)). Qed.
intros k l1 l2. rewrite !(comm (++) _ k). by apply (inj (k ++)).
Qed.
Lemma replicate_Permutation n x l : replicate n x l replicate n x = l. Lemma replicate_Permutation n x l : replicate n x l replicate n x = l.
Proof. Proof.
intros Hl. apply replicate_as_elem_of. split. intros Hl. apply replicate_as_elem_of. split.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment