Commit 8e8305ce authored by Robbert Krebbers's avatar Robbert Krebbers

Make f_equiv slightly more robust.

Now, for example, when having equiv (Some x) (Some y) it will
try to find a Proper whose range is an equiv before hitting the
eq instance. My hack is general enough that it works for Forall2,
dist, and so on, too.
parent f4320358
......@@ -251,8 +251,10 @@ Ltac setoid_subst :=
end.
(** f_equiv works on goals of the form "f _ = f _", for any relation and any
number of arguments. It looks for an appropriate "Proper" instance, and
applies it. *)
number of arguments. It looks for an appropriate "Proper" instance, and applies
it. The tactic is somewhat limited, since it cannot be used to backtrack on
the Proper instances that has been found. To that end, we try to ensure the
trivial instance in which the resulting goals have an [eq]. *)
Ltac f_equiv :=
match goal with
| _ => reflexivity
......@@ -263,10 +265,16 @@ Ltac f_equiv :=
| |- ?R (match ?x with _ => _ end) (match ?x with _ => _ end) =>
destruct x
(* First assume that the arguments need the same relation as the result *)
| |- ?R (?f ?x) (?f _) =>
apply (_ : Proper (R ==> R) f)
| |- ?R (?f ?x ?y) (?f _ _) =>
apply (_ : Proper (R ==> R ==> R) f)
| |- ?R (?f ?x) (?f _) => apply (_ : Proper (R ==> R) f)
(* For the case in which R is polymorphic, or an operational type class,
like equiv. *)
| |- (?R _) (?f ?x) (?f _) => apply (_ : Proper (R _ ==> _) f)
| |- (?R _ _) (?f ?x) (?f _) => apply (_ : Proper (R _ _ ==> _) f)
| |- (?R _ _ _) (?f ?x) (?f _) => apply (_ : Proper (R _ _ _ ==> _) f)
| |- (?R _) (?f ?x ?y) (?f _ _) => apply (_ : Proper (R _ ==> R _ ==> _) f)
| |- (?R _ _) (?f ?x ?y) (?f _ _) => apply (_ : Proper (R _ _ ==> R _ _ ==> _) f)
| |- (?R _ _ _) (?f ?x ?y) (?f _ _) => apply (_ : Proper (R _ _ _ ==> R _ _ _ ==> _) f)
| |- (?R _ _ _ _) (?f ?x ?y) (?f _ _) => apply (_ : Proper (R _ _ _ _ ==> R _ _ _ _ ==> _) f)
(* Next, try to infer the relation. Unfortunately, there is an instance
of Proper for (eq ==> _), which will always be matched. *)
(* TODO: Can we exclude that instance? *)
......
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