Commit 3caefaaa authored by Robbert Krebbers's avatar Robbert Krebbers

New definition of contractive.

Using this new definition we can express being contractive using a
Proper. This has the following advantages:

- It makes it easier to state that a function with multiple arguments
  is contractive (in all or some arguments).
- A solve_contractive tactic can be implemented by extending the
  solve_proper tactic.
parent 3f13bd94
...@@ -185,8 +185,8 @@ Proof. ...@@ -185,8 +185,8 @@ Proof.
rewrite !map_to_list_insert, !bind_cons rewrite !map_to_list_insert, !bind_cons
by (by rewrite ?lookup_union_with, ?lookup_delete, ?HX). by (by rewrite ?lookup_union_with, ?lookup_delete, ?HX).
rewrite (assoc_L _), <-(comm (++) (f (_,n'))), <-!(assoc_L _), <-IH. rewrite (assoc_L _), <-(comm (++) (f (_,n'))), <-!(assoc_L _), <-IH.
rewrite (assoc_L _); f_equiv; [rewrite (comm _); simpl|done]. rewrite (assoc_L _). f_equiv.
by rewrite replicate_plus, Permutation_middle. rewrite (comm _); simpl. by rewrite replicate_plus, Permutation_middle.
- rewrite <-insert_union_with_l, !map_to_list_insert, !bind_cons - rewrite <-insert_union_with_l, !map_to_list_insert, !bind_cons
by (by rewrite ?lookup_union_with, ?HX, ?HY). by (by rewrite ?lookup_union_with, ?HX, ?HY).
by rewrite <-(assoc_L (++)), <-IH. by rewrite <-(assoc_L (++)), <-IH.
......
...@@ -273,6 +273,7 @@ favor the second because the relation (dist) stays the same. *) ...@@ -273,6 +273,7 @@ favor the second because the relation (dist) stays the same. *)
Ltac f_equiv := Ltac f_equiv :=
match goal with match goal with
| _ => reflexivity | _ => reflexivity
| |- pointwise_relation _ _ _ _ => intros ?
(* We support matches on both sides, *if* they concern the same variable, or (* We support matches on both sides, *if* they concern the same variable, or
variables in some relation. *) variables in some relation. *)
| |- ?R (match ?x with _ => _ end) (match ?x with _ => _ end) => | |- ?R (match ?x with _ => _ end) (match ?x with _ => _ end) =>
...@@ -301,26 +302,12 @@ Ltac f_equiv := ...@@ -301,26 +302,12 @@ Ltac f_equiv :=
(* 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) => apply H | H : pointwise_relation _ ?R ?f ?g |- ?R (?f ?x) (?g ?x) => apply H
end.
(** auto_proper solves goals of the form "f _ = f _", for any relation and any
number of arguments, by repeatedly applying f_equiv and handling trivial cases.
If it cannot solve an equality, it will leave that to the user. *)
Ltac auto_equiv :=
(* Deal with "pointwise_relation" *)
repeat lazymatch goal with
| |- pointwise_relation _ _ _ _ => intros ?
end; end;
(* Normalize away equalities. *) try reflexivity.
simplify_eq;
(* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *) (* The tactic [preprocess_solve_proper] unfolds the first head symbol, so that
try (f_equiv; fast_done || auto_equiv). we proceed by repeatedly using [f_equiv]. *)
Ltac preprocess_solve_proper :=
(** solve_proper solves goals of the form "Proper (R1 ==> R2)", for any
number of relations. All the actual work is done by auto_equiv;
solve_proper just introduces the assumptions and unfolds the first
head symbol. *)
Ltac solve_proper :=
(* Introduce everything *) (* Introduce everything *)
intros; intros;
repeat lazymatch goal with repeat lazymatch goal with
...@@ -340,7 +327,14 @@ Ltac solve_proper := ...@@ -340,7 +327,14 @@ 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 [ auto_equiv ]. simplify_eq.
(** The tactic [solve_proper] solves goals of the form "Proper (R1 ==> R2)", for
any number of relations. The actual work is done by repeatedly applying
[f_equiv]. *)
Ltac solve_proper :=
preprocess_solve_proper;
solve [repeat (f_equiv; try eassumption)].
(** 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