Commit 0c7a5b02 authored by Robbert Krebbers's avatar Robbert Krebbers

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents aa947529 d0c9c6c8
Pipeline #175 passed with stage
...@@ -77,7 +77,7 @@ Proof. by intros ??? ?? [??]; split; apply up_preserving. Qed. ...@@ -77,7 +77,7 @@ Proof. by intros ??? ?? [??]; split; apply up_preserving. Qed.
Global Instance up_set_preserving : Proper (() ==> flip () ==> ()) up_set. Global Instance up_set_preserving : Proper (() ==> flip () ==> ()) up_set.
Proof. Proof.
intros S1 S2 HS T1 T2 HT. rewrite /up_set. intros S1 S2 HS T1 T2 HT. rewrite /up_set.
f_equiv. move =>s1 s2 Hs. simpl in HT. by apply up_preserving. f_equiv; last done. move =>s1 s2 Hs. simpl in HT. by apply up_preserving.
Qed. Qed.
Global Instance up_set_proper : Proper (() ==> () ==> ()) up_set. Global Instance up_set_proper : Proper (() ==> () ==> ()) up_set.
Proof. by intros S1 S2 [??] T1 T2 [??]; split; apply up_set_preserving. Qed. Proof. by intros S1 S2 [??] T1 T2 [??]; split; apply up_set_preserving. Qed.
......
...@@ -229,30 +229,23 @@ Ltac setoid_subst := ...@@ -229,30 +229,23 @@ Ltac setoid_subst :=
| H : @equiv ?A ?e _ ?x |- _ => symmetry in H; setoid_subst_aux (@equiv A e) x | H : @equiv ?A ?e _ ?x |- _ => symmetry in H; setoid_subst_aux (@equiv A e) x
end. end.
(** f_equiv solves goals of the form "f _ = f _", for any relation and any (** f_equiv works on goals of the form "f _ = f _", for any relation and any
number of arguments, by looking for appropriate "Proper" instances. number of arguments. It looks for an appropriate "Proper" instance, and
If it cannot solve an equality, it will leave that to the user. *) applies it. *)
Ltac f_equiv := Ltac f_equiv :=
(* Deal with "pointwise_relation" *) match goal with
repeat lazymatch goal with | _ => reflexivity
| |- pointwise_relation _ _ _ _ => intros ?
end;
(* Normalize away equalities. *)
simplify_eq;
(* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *)
try match goal with
| _ => first [ reflexivity | assumption | symmetry; assumption]
(* We support matches on both sides, *if* they concern the same (* We support matches on both sides, *if* they concern the same
variable. variable.
TODO: We should support different variables, provided that we can TODO: We should support different variables, provided that we can
derive contradictions for the off-diagonal cases. *) derive contradictions for the off-diagonal cases. *)
| |- ?R (match ?x with _ => _ end) (match ?x with _ => _ end) => | |- ?R (match ?x with _ => _ end) (match ?x with _ => _ end) =>
destruct x; f_equiv destruct x
(* First assume that the arguments need the same relation as the result *) (* First assume that the arguments need the same relation as the result *)
| |- ?R (?f ?x) (?f _) => | |- ?R (?f ?x) (?f _) =>
apply (_ : Proper (R ==> R) f); f_equiv apply (_ : Proper (R ==> R) f)
| |- ?R (?f ?x ?y) (?f _ _) => | |- ?R (?f ?x ?y) (?f _ _) =>
apply (_ : Proper (R ==> R ==> R) f); f_equiv apply (_ : Proper (R ==> R ==> R) f)
(* Next, try to infer the relation. Unfortunately, there is an instance (* Next, try to infer the relation. Unfortunately, there is an instance
of Proper for (eq ==> _), which will always be matched. *) of Proper for (eq ==> _), which will always be matched. *)
(* TODO: Can we exclude that instance? *) (* TODO: Can we exclude that instance? *)
...@@ -260,15 +253,28 @@ Ltac f_equiv := ...@@ -260,15 +253,28 @@ Ltac f_equiv :=
query for "pointwise_relation"'s. But that leads to a combinatorial query for "pointwise_relation"'s. But that leads to a combinatorial
explosion about which arguments are and which are not the same. *) explosion about which arguments are and which are not the same. *)
| |- ?R (?f ?x) (?f _) => | |- ?R (?f ?x) (?f _) =>
apply (_ : Proper (_ ==> R) f); f_equiv apply (_ : Proper (_ ==> R) f)
| |- ?R (?f ?x ?y) (?f _ _) => | |- ?R (?f ?x ?y) (?f _ _) =>
apply (_ : Proper (_ ==> _ ==> R) f); f_equiv apply (_ : Proper (_ ==> _ ==> R) f)
(* In case the function symbol differs, but the arguments are the same, (* In case the function symbol differs, but the arguments are the same,
maybe we have a pointwise_relation in our context. *) maybe we have a pointwise_relation in our context. *)
| H : pointwise_relation _ ?R ?f ?g |- ?R (?f ?x) (?g ?x) => | H : pointwise_relation _ ?R ?f ?g |- ?R (?f ?x) (?g ?x) =>
apply H; f_equiv apply H
end. end.
(** auto_proper solves goals of the form "f _ = f _", for any relation and any
number of arguments, by repeatedly apply f_equiv and handling trivial cases.
If it cannot solve an equality, it will leave that to the user. *)
Ltac auto_proper :=
(* Deal with "pointwise_relation" *)
repeat lazymatch goal with
| |- pointwise_relation _ _ _ _ => intros ?
end;
(* Normalize away equalities. *)
simplify_eq;
(* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *)
try (f_equiv; assumption || (symmetry; assumption) || auto_proper).
(** solve_proper solves goals of the form "Proper (R1 ==> R2)", for any (** solve_proper solves goals of the form "Proper (R1 ==> R2)", for any
number of relations. All the actual work is done by f_equiv; number of relations. All the actual work is done by f_equiv;
solve_proper just introduces the assumptions and unfolds the first solve_proper just introduces the assumptions and unfolds the first
...@@ -291,7 +297,7 @@ Ltac solve_proper := ...@@ -291,7 +297,7 @@ Ltac solve_proper :=
| |- ?R (?f _ _) (?f _ _) => unfold f | |- ?R (?f _ _) (?f _ _) => unfold f
| |- ?R (?f _) (?f _) => unfold f | |- ?R (?f _) (?f _) => unfold f
end; end;
solve [ f_equiv ]. solve [ auto_proper ].
(** The tactic [intros_revert tac] introduces all foralls/arrows, performs tac, (** The tactic [intros_revert tac] introduces all foralls/arrows, performs tac,
and then reverts them. *) and then reverts them. *)
......
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