Commit cd3dd884 authored by Dan Frumin's avatar Dan Frumin

A bit of cleanup

parent a3eb6851
......@@ -63,7 +63,6 @@ Section bit_refinement.
Lemma bit_prerefinement Γ E1 :
{E1,E1;Δ;Γ} bit_bool log bit_nat : bitτ.
Proof.
simpl.
iApply (bin_log_related_pack _ bitτi).
repeat iApply bin_log_related_pair.
- rel_vals; simpl; eauto.
......
......@@ -11,6 +11,8 @@
- v1 or (λ_, v2 or v3) associativity
(λ_, v1 or v2) or v3
- v1 () v1 or v2 choice on the RHS
where every v_i is well-typed Unit -> Unit
*)
From iris.proofmode Require Import tactics.
From iris_logrel Require Export logrel examples.various (* for bot *).
......@@ -29,7 +31,7 @@ Lemma or_type Γ :
Proof. solve_typed. Qed.
Hint Resolve or_type : typeable.
Section rules.
Section contents.
Context `{logrelG Σ}.
Lemma bin_log_related_or Δ Γ E e1 e2 e1' e2' :
......@@ -298,15 +300,6 @@ Section rules.
iApply bin_log_related_unit.
Qed.
(* The associativity in the other direction, assuming commutativity:
(v1 or v2) or v3
(v2 or v1) or v3 comm
v3 or (v2 or v1) comm
(v3 or v2) or v1 assoc1
(v2 or v3) or v1 comm
v1 or (v2 or v3)
*)
Lemma bin_log_let1 Δ Γ E (v : val) (e : expr) τ :
Closed {["x"]} e
logrelN E
......@@ -333,5 +326,90 @@ Section rules.
by iApply binary_fundamental_masked.
Qed.
End rules.
End contents.
Section theory.
Lemma or_idempotency_1 (v : val) :
⊢ₜ v : TArrow TUnit TUnit
or v v ctx v #() : TUnit.
Proof.
intros Ht.
eapply (logrel_ctxequiv logrelΣ); [solve_closed.. | intros ].
iApply bin_log_or_idem_l; eauto.
by iApply binary_fundamental.
Qed.
Lemma or_idempotency_2 (v : val) :
⊢ₜ v : TArrow TUnit TUnit
v #() ctx or v v : TUnit.
Proof.
intros Ht.
eapply (logrel_ctxequiv logrelΣ); [solve_closed.. | intros ].
iApply bin_log_or_idem_r; eauto.
by iApply binary_fundamental.
Qed.
Lemma or_commutativity (v1 v2 : val) :
⊢ₜ v1 : TArrow TUnit TUnit
⊢ₜ v2 : TArrow TUnit TUnit
or v1 v2 ctx or v2 v1 : TUnit.
Proof.
intros Ht1 Ht2.
eapply (logrel_ctxequiv logrelΣ); [solve_closed.. | intros ].
iApply bin_log_or_commute; eauto; by iApply binary_fundamental.
Qed.
Lemma or_unital_1 (v : val) :
⊢ₜ v : TArrow TUnit TUnit
or v bot ctx v #() : TUnit.
Proof.
intros Ht.
eapply (logrel_ctxequiv logrelΣ); [solve_closed.. | intros ].
iApply bin_log_or_bot_l; eauto.
by iApply binary_fundamental.
Qed.
Lemma or_unital_2 (v : val) :
⊢ₜ v : TArrow TUnit TUnit
v #() ctx or v bot : TUnit.
Proof.
intros Ht.
eapply (logrel_ctxequiv logrelΣ); [solve_closed.. | intros ].
iApply bin_log_or_bot_r; eauto.
by iApply binary_fundamental.
Qed.
Lemma or_choice_1 (v1 v2 : val) :
⊢ₜ v1 : TArrow TUnit TUnit
v1 #() ctx or v1 v2 : TUnit.
Proof.
intros Ht.
eapply (logrel_ctxequiv logrelΣ); [solve_closed.. | intros ].
iApply bin_log_or_choice_1_r_val; eauto.
by iApply binary_fundamental.
Qed.
Lemma or_assoc_1 (v1 v2 v3 : val) :
⊢ₜ v1 : TArrow TUnit TUnit
⊢ₜ v2 : TArrow TUnit TUnit
⊢ₜ v3 : TArrow TUnit TUnit
(or v1 (λ: <>, or v2 v3))%E ctx (or (λ: <>, or v1 v2) v3)%E : TUnit.
Proof.
intros Ht1 Ht2 Ht3.
eapply (logrel_ctxequiv logrelΣ); [solve_closed.. | intros ].
iApply bin_log_or_assoc1; eauto; by iApply binary_fundamental.
Qed.
(* The associativity in the other direction, assuming commutativity:
(v1 or v2) or v3
(v2 or v1) or v3 comm
v3 or (v2 or v1) comm
(v3 or v2) or v1 assoc1
(v2 or v3) or v1 comm
v1 or (v2 or v3)
*)
(* Lemma or_assoc_2 (v1 v2 v3 : val) : *)
(* ⊢ₜ v1 : TArrow TUnit TUnit *)
(* ⊢ₜ v2 : TArrow TUnit TUnit *)
(* ⊢ₜ v3 : TArrow TUnit TUnit *)
(* (or (λ: <>, or v1 v2) v3)%E ctx (or v1 (λ: <>, or v2 v3))%E : TUnit. *)
End theory.
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