diff options
author | Andres Erbsen <andreser@mit.edu> | 2016-10-29 17:54:42 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2016-10-29 17:54:42 -0400 |
commit | b34da8a551b3c8aa2086155ff523030126b19f2e (patch) | |
tree | 765185361d823b85cce3ee7b2ace0fc36844fe7d /src/Util | |
parent | a0bf587c8223ae237a475bb523784502a7a7dd68 (diff) |
prove Proper_SRepERepMul
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/IterAssocOp.v | 58 | ||||
-rw-r--r-- | src/Util/Relations.v | 16 |
2 files changed, 73 insertions, 1 deletions
diff --git a/src/Util/IterAssocOp.v b/src/Util/IterAssocOp.v index e520ca9f9..773fea8fd 100644 --- a/src/Util/IterAssocOp.v +++ b/src/Util/IterAssocOp.v @@ -191,4 +191,60 @@ Section IterAssocOp. rewrite Nshiftr_size by auto. reflexivity. Qed. -End IterAssocOp.
\ No newline at end of file +End IterAssocOp. + +Require Import Coq.Classes.Morphisms. +Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.Relations. + +Global Instance Proper_funexp {T R} {Equivalence_R:Equivalence R} + : Proper ((R==>R) ==> R ==> Logic.eq ==> R) (@funexp T). +Proof. + repeat intro; subst. + match goal with [n0 : nat |- _ ] => rename n0 into n; induction n end; [solve [trivial]|]. + match goal with + [H: (_ ==> _)%signature _ _ |- _ ] => + etransitivity; solve [eapply (H _ _ IHn)|reflexivity] + end. +Qed. + +Global Instance Proper_test_and_op {T R} {Equivalence_R:@Equivalence T R} : + Proper ((R==>R==>R) + ==> pointwise_relation _ Logic.eq + ==> (Logic.eq==>R==>R==>R) + ==> R + ==> (fun nt NT => Logic.eq (fst nt) (fst NT) /\ R (snd nt) (snd NT)) + ==> (fun nt NT => Logic.eq (fst nt) (fst NT) /\ R (snd nt) (snd NT)) + ) (@test_and_op T). +Proof. + repeat match goal with + | _ => intro + | _ => split + | [p:prod _ _ |- _ ] => destruct p + | [p:and _ _ |- _ ] => destruct p + | _ => progress (cbv [fst snd test_and_op pointwise_relation respectful] in * ) + | _ => progress subst + | _ => progress break_match + | _ => solve [ congruence | eauto 99 ] + end. +Qed. + +Global Instance Proper_iter_op {T R} {Equivalence_R:@Equivalence T R} : + Proper ((R==>R==>R) + ==> R + ==> pointwise_relation _ Logic.eq + ==> (Logic.eq==>R==>R==>R) + ==> Logic.eq + ==> R + ==> R) + (@iter_op T). +Proof. + repeat match goal with + | _ => solve [ reflexivity | congruence | eauto 99 ] + | _ => progress eapply (Proper_funexp (R:=(fun nt NT => Logic.eq (fst nt) (fst NT) /\ R (snd nt) (snd NT)))) + | _ => progress eapply Proper_test_and_op + | _ => progress eapply conj + | _ => progress (cbv [fst snd pointwise_relation respectful] in * ) + | _ => intro + end. +Qed.
\ No newline at end of file diff --git a/src/Util/Relations.v b/src/Util/Relations.v index 4612fa8a8..4926bd74c 100644 --- a/src/Util/Relations.v +++ b/src/Util/Relations.v @@ -31,4 +31,20 @@ Qed. Lemma iff_R_R_same_r {T R} {Req:@Equivalence T R} x y ref : R x y -> (R x ref <-> R y ref). Proof. intro Hx; rewrite Hx; clear Hx. reflexivity. +Qed. + +Global Instance Equivalence_and {A B RA RB} + {Equivalence_RA:@Equivalence A RA} + {Equivalence_RB:@Equivalence B RB} + : Equivalence (fun ab AB => RA (fst ab) (fst AB) /\ RB (snd ab) (snd AB)). +Proof. + destruct Equivalence_RA as [], Equivalence_RB as []; cbv in *|-. + repeat match goal with + | _ => intro + | _ => split + | [p:prod _ _ |- _ ] => destruct p + | [p:and _ _ |- _ ] => destruct p + | _ => progress (cbv [fst snd] in * ) + | _ => solve[eauto] + end. Qed.
\ No newline at end of file |