Commit f2f3b6bf authored by Dan Frumin's avatar Dan Frumin

Simplify solve_proper_alt

parent 479a6a8c
......@@ -17,19 +17,7 @@ Ltac auto_equiv :=
(* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *)
try (f_equiv; fast_done || auto_equiv).
(* TODO: modify this in coq-stdpp or something *)
(* this is /almost/ [solve_proper_core ltac:(fun _ => auto_equiv)] *)
(* but we do an additional simpl auto [simplify_eq] *)
Ltac solve_proper ::=
intros;
repeat lazymatch goal with
| |- Proper _ _ => intros ???
| |- (_ ==> _)%signature _ _ => intros ???
| |- pointwise_relation _ _ _ _ => intros ?
| |- ?R ?f _ => try let f' := constr:(λ x, f x) in intros ?
end; simplify_eq/=;
(solve_proper_unfold + idtac);
solve [repeat first [eassumption | auto_equiv] ].
Ltac solve_proper ::= solve_proper_core ltac:(fun _ => simpl; auto_equiv).
Definition logN : namespace := logrelN .@ "logN".
......@@ -46,7 +34,7 @@ Section semtypes.
|={E1,E2}=> WP ee.1 {{ v, v', j fill K (of_val v') τi Δ (v, v') }})%I.
Global Instance interp_expr_ne n E1 E2:
Proper (dist n ==> dist n ==> (=) ==> dist n) (interp_expr E1 E2).
Proof. solve_proper. Qed.
Proof. solve_proper. Qed.
Program Definition ctx_lookup (x : var) : listC D -n> D := λne Δ ww,
( from_option id (cconst True)%I (Δ !! x) ww)%I.
......@@ -54,7 +42,7 @@ Section semtypes.
Program Definition interp_unit : listC D -n> D := λne Δ ww,
(ww.1 = #() ww.2 = #())%I.
Solve Obligations with solve_proper_alt.
Solve Obligations with solve_proper.
Program Definition interp_nat : listC D -n> D := λne Δ ww,
( n : nat, ww.1 = #n ww.2 = #n)%I.
......
......@@ -37,10 +37,6 @@ Ltac properness :=
| |- (inv _ _)%I (inv _ _)%I => apply (contractive_proper _)
end.
Ltac solve_proper_alt :=
repeat intro; (simpl + idtac);
by repeat match goal with H : _ {_} _|- _ => rewrite H end.
Reserved Notation "⟦ τ ⟧" (at level 0, τ at level 70).
Reserved Notation "⟦ τ ⟧ₑ" (at level 0, τ at level 70).
Reserved Notation "⟦ Γ ⟧*" (at level 0, Γ at level 70).
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