Commit cafae3e7 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

More WIP.

parent d16ab1aa
......@@ -44,16 +44,26 @@ Section setoid_tests.
Definition setoid_test1 (rec : myfunS nat A) : myfunS nat A :=
λ n, h (f (rec n)) (rec n).
Goal Proper (setoid_equiv ==> setoid_equiv) setoid_test1.
#[local] Instance: Proper (setoid_equiv ==> setoid_equiv) setoid_test1.
Proof. solve_proper. Qed.
Definition setoid_test2 (rec : myfunS nat (myfunS nat A)) : myfunS nat A :=
λ n, h (f (rec n n)) (rec n n).
Goal Proper (setoid_equiv ==> setoid_equiv) setoid_test2.
#[local] Instance: Proper (setoid_equiv ==> setoid_equiv) setoid_test2.
Proof. solve_proper. Qed.
Definition setoid_test3 (rec : myfunS nat A) : myfunS nat (myfunS nat A) :=
λ n m, h (f (rec n)) (rec m).
Goal Proper (setoid_equiv ==> setoid_equiv) setoid_test3.
#[local] Instance: Proper (setoid_equiv ==> setoid_equiv) setoid_test3.
Proof. solve_proper. Qed.
Definition setoid_test4 (rec : myfunS nat A) : myfunS nat (myfunS nat A) :=
λ n, setoid_test2 (λ m, setoid_test1 rec).
#[local] Instance: Proper (setoid_equiv ==> setoid_equiv) setoid_test4.
Proof. solve_proper. Qed.
Definition setoid_test5 (rec : myfunS nat A) : myfunS nat A :=
setoid_test2 (setoid_test3 rec).
#[local] Instance: Proper (setoid_equiv ==> setoid_equiv) setoid_test4.
Proof. solve_proper. Qed.
End setoid_tests.
......@@ -1044,6 +1044,14 @@ Section pred_finite_infinite.
pred_infinite P ( x, P x Q x) pred_infinite Q.
Proof. unfold pred_infinite. set_solver. Qed.
Lemma pred_infinite_surj {A B} (P : B Prop) (f : A B) :
( x, P x y, f y = x)
pred_infinite P pred_infinite (P f).
Proof.
intros Hf HP xs. generalize (HP (f <$> xs)).
setoid_rewrite elem_of_list_fmap. naive_solver.
Qed.
Lemma pred_not_infinite_finite {A} (P : A Prop) :
pred_infinite P pred_finite P False.
Proof. intros Hinf [xs ?]. destruct (Hinf xs). set_solver. Qed.
......
......@@ -369,18 +369,24 @@ Ltac f_equiv :=
| |- (?R _ _) (?f _ _ _ _) _ => simple apply (_ : Proper (R _ _ ==> R _ _ ==> R _ _ ==> R _ _ ==> _) f)
| |- (?R _ _ _) (?f _ _ _ _) _ => simple apply (_ : Proper (R _ _ _ ==> R _ _ _ R _ _ _ ==> R _ _ _ ==> _) f)
(* If we cannot find a [Proper] instance that involves the relation [R],
check if [R] is convertable to a [pointwise_relation], i.e., [R] is a
check if [R] is a relation on functions. is convertable to a [pointwise_relation], i.e., [R] is a
point-wise relation on functions. In this case, we introduce the function
argument, and [simpl]ify the resulting goal. *)
| |- ?R _ _ => eunify R (pointwise_relation _ _); intros ?; csimpl
(* Next, try to infer the relation by searching for an arbitrary [Proper]
instance. Unfortunately, very often, it will turn the goal into a Leibniz
equality so we get stuck. *)
(* TODO: Can we exclude that instance? *)
| |- ?R (?f _) _ => simple apply (_ : Proper (_ ==> R) f)
| |- ?R (?f _ _) _ => simple apply (_ : Proper (_ ==> _ ==> R) f)
| |- ?R (?f _ _ _) _ => simple apply (_ : Proper (_ ==> _ ==> _ ==> R) f)
| |- ?R (?f _ _ _ _) _ => simple apply (_ : Proper (_ ==> _ ==> _ ==> _ ==> R) f)
argument, and [simpl]ify the resulting goal.
Deal with other cases where we have an equivalence relation on functions
(e.g. a [pointwise_relation] that is hidden in some form in [R]). We do
this by checking if the arguments of the relation are actually functions,
and then forcefully introduce one ∀ and introduce the remaining ∀s that
show up in the goal.
*)
| |- ?R ?f _ =>
(* To check that we actually have an equivalence relation
on functions, we try to eta expand [f], which will only succeed if [f] is
actually a function. *)
let f' := constr:(λ x, f x) in
(* Now forcefully introduce the first ∀ and other ∀s that show up in the
goal afterwards. *)
intros ?; csimpl
(* In case the function symbol differs, but the arguments are the same,
maybe we have a [pointwise_relation] in our context. *)
(* TODO: If only some of the arguments are the same, we could also
......@@ -390,6 +396,14 @@ Ltac f_equiv :=
| H : ?R' ?f ?g |- ?R (?f _ _) (?g _ _) => eunify R' (pointwise_relation _ _); simple apply H
| H : ?R' ?f ?g |- ?R (?f _ _ _) (?g _ _ _) => eunify R' (pointwise_relation _ _); simple apply H
| H : ?R' ?f ?g |- ?R (?f _ _ _ _) (?g _ _ _ _) => eunify R' (pointwise_relation _ _); simple apply H
(* Next, if all fails, try to infer the relation by searching for an arbitrary
[Proper] instance. Unfortunately, very often, it will turn the goal into a
Leibniz equality so we get stuck. *)
(* TODO: Can we exclude that instance? *)
| |- ?R (?f _) _ => simple apply (_ : Proper (_ ==> R) f)
| |- ?R (?f _ _) _ => simple apply (_ : Proper (_ ==> _ ==> R) f)
| |- ?R (?f _ _ _) _ => simple apply (_ : Proper (_ ==> _ ==> _ ==> R) f)
| |- ?R (?f _ _ _ _) _ => simple apply (_ : Proper (_ ==> _ ==> _ ==> _ ==> R) f)
end;
try simple apply reflexivity.
Tactic Notation "f_equiv" "/=" := csimpl in *; f_equiv.
......@@ -410,6 +424,7 @@ Ltac solve_proper_unfold :=
| |- ?R (?f _ _) (?f _ _) => unfold f
| |- ?R (?f _) (?f _) => unfold f
end.
(** [solve_proper_prepare] does some preparation work before the main
[solve_proper] loop. Having this as a separate tactic is useful for debugging
[solve_proper] failure. *)
......@@ -419,23 +434,11 @@ Ltac solve_proper_prepare :=
repeat lazymatch goal with
| |- Proper _ _ => intros ???
| |- (_ ==> _)%signature _ _ => intros ???
| |- pointwise_relation _ _ _ _ => intros ?
| |- ?R ?f _ =>
(* Deal with other cases where we have an equivalence relation on functions
(e.g. a [pointwise_relation] that is hidden in some form in [R]). We do
this by checking if the arguments of the relation are actually functions,
and then forcefully introduce one ∀ and introduce the remaining ∀s that
show up in the goal. To check that we actually have an equivalence relation
on functions, we try to eta expand [f], which will only succeed if [f] is
actually a function. *)
let f' := constr:(λ x, f x) in
(* Now forcefully introduce the first ∀ and other ∀s that show up in the
goal afterwards. *)
intros ?; intros
end; simplify_eq;
(* We try with and without unfolding. We have to backtrack on
that because unfolding may succeed, but then the proof may fail. *)
(solve_proper_unfold + idtac); simpl.
(** The tactic [solve_proper_core tac] solves goals of the form "Proper (R1 ==> R2)", for
any number of relations. The actual work is done by repeatedly applying
[tac]. *)
......
Supports Markdown
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