Commit 9aed61c5 authored by Ralf Jung's avatar Ralf Jung

more f_equiv work.

parent 8d983adf
......@@ -236,17 +236,17 @@ Ltac f_equiv :=
try lazymatch goal with
| |- pointwise_relation _ _ _ _ => intros ?
end;
(* Normalize away equalities. *)
subst;
(* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *)
first [ reflexivity | assumption | symmetry; assumption |
match goal with
(* We support matches on both sides, *if* they concern the same
or provably equal variables.
variable.
TODO: We should support different variables, provided that we can
derive contradictions for the off-diagonal cases. *)
| |- ?R (match ?x with _ => _ end) (match ?x with _ => _ end) =>
destruct x; f_equiv
| |- ?R (match ?x with _ => _ end) (match ?y with _ => _ end) =>
subst y; f_equiv
(* First assume that the arguments need the same relation as the result *)
| |- ?R (?f ?x) (?f _) =>
let H := fresh "Proper" in
......
......@@ -27,7 +27,7 @@ Import uPred.
Global Instance ht_ne E n :
Proper (dist n ==> eq==>pointwise_relation _ (dist n) ==> dist n) (@ht Λ Σ E).
Proof. by intros P P' HP e ? <- Φ Φ' HΦ; rewrite /ht HP; setoid_rewrite HΦ. Qed.
Proof. solve_proper. Qed.
Global Instance ht_proper E :
Proper (() ==> eq ==> pointwise_relation _ () ==> ()) (@ht Λ Σ E).
Proof. by intros P P' HP e ? <- Φ Φ' HΦ; rewrite /ht HP; setoid_rewrite HΦ. Qed.
......
......@@ -30,7 +30,7 @@ Qed.
Global Instance vs_ne E1 E2 n :
Proper (dist n ==> dist n ==> dist n) (@vs Λ Σ E1 E2).
Proof. by intros P P' HP Q Q' HQ; rewrite /vs HP HQ. Qed.
Proof. solve_proper. Qed.
Global Instance vs_proper E1 E2 : Proper (() ==> () ==> ()) (@vs Λ Σ E1 E2).
Proof. apply ne_proper_2, _. Qed.
......
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