Commit d136c946 authored by Dan Frumin's avatar Dan Frumin

Notation for negation

parent 4014e9e9
......@@ -59,6 +59,7 @@ Notation "e1 ≤ e2" := (BinOp Le e1%E e2%E) (at level 70) : expr_scope.
Notation "e1 < e2" := (BinOp Lt e1%E e2%E) (at level 70) : expr_scope.
Notation "e1 = e2" := (BinOp Eq e1%E e2%E) (at level 70) : expr_scope.
Notation "e1 ⊕ e2" := (BinOp Xor e1%E e2%E) (at level 70) : expr_scope.
Notation "¬ e" := (BinOp Xor e%E (Lit (Bool true))) (at level 75, right associativity) : expr_scope.
(* The unicode is already part of the notation "_ ← _; _" for bind. *)
Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope.
......
......@@ -24,12 +24,10 @@ Section refinement.
Definition bitτ : type := : TVar 0 × (TVar 0 TVar 0) × (TVar 0 Bool).
Definition bit_bool : val :=
pack (#true, (λ: "b", "b" #true), (λ: "b", "b")).
pack (#true, (λ: "b", ¬ "b"), (λ: "b", "b")).
Definition flip_nat : val := λ: "n",
if: ("n" = #0) then #1 else #0.
Definition bit_nat : val :=
pack (#1, flip_nat, (λ: "b", "b" = #1)).
pack (#1, (λ: "n", if: ("n" = #0) then #1 else #0), (λ: "b", "b" = #1)).
Definition f (b : bool) : nat := if b then 1 else 0.
(* R Bool × Nat = { (true, 1), (false, 0) }*)
......@@ -42,18 +40,18 @@ Section refinement.
Lemma bit_prerefinement Δ Γ :
{Δ;Γ} bit_bool log bit_nat : bitτ.
Proof.
unfold bit_bool, bit_nat, flip_nat; simpl. (* we need this to compute the coercion from values to expression *)
unfold bit_bool, bit_nat; simpl. (* we need this to compute the coercion from values to expression *)
iApply (bin_log_related_pack _ R).
repeat iApply bin_log_related_pair.
- rel_finish.
- iApply bin_log_related_arrow_val; try by unlock. cbn-[R].
iIntros "!#" (v1 v2) "/=".
iIntros "!#" (v1 v2).
iIntros ([b [? ?]]); simplify_eq/=. unlock; simpl.
rel_rec_l. rel_rec_r.
rel_op_l. rel_op_r.
destruct b; simpl; rel_if_r; rel_finish.
- iApply bin_log_related_arrow_val; try by unlock.
iIntros "!#" (v1 v2) "/=". (* TODO: notation for LitV? *)
iIntros "!#" (v1 v2).
iIntros ([b [? ?]]); simplify_eq/=. unlock; simpl.
rel_rec_l. rel_rec_r.
rel_op_r.
......
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