Commit 1c87b96a authored by Robbert Krebbers's avatar Robbert Krebbers

Define dist on option using option_Forall2.

parent 0b8de700
......@@ -454,13 +454,10 @@ Canonical Structure boolC := leibnizC bool.
Section option.
Context {A : cofeT}.
Inductive option_dist' (n : nat) : relation (option A) :=
| Some_dist x y : x {n} y option_dist' n (Some x) (Some y)
| None_dist : option_dist' n None None.
Instance option_dist : Dist (option A) := option_dist'.
Instance option_dist : Dist (option A) := λ n, option_Forall2 (dist n).
Lemma dist_option_Forall2 n mx my : mx {n} my option_Forall2 (dist n) mx my.
Proof. split; destruct 1; constructor; auto. Qed.
Proof. done. Qed.
Program Definition option_chain (c : chain (option A)) (x : A) : chain A :=
{| chain_car n := from_option x (c n) |}.
......@@ -474,10 +471,7 @@ Section option.
- intros mx my; split; [by destruct 1; constructor; apply equiv_dist|].
intros Hxy; destruct (Hxy 0); constructor; apply equiv_dist.
by intros n; feed inversion (Hxy n).
- intros n; split.
+ by intros [x|]; constructor.
+ by destruct 1; constructor.
+ destruct 1; inversion_clear 1; constructor; etrans; eauto.
- apply _.
- destruct 1; constructor; by apply dist_S.
- intros n c; rewrite /compl /option_compl.
feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
......@@ -503,6 +497,7 @@ Section option.
Proof. by intros ?; inversion_clear 1; constructor; apply timeless. Qed.
End option.
Typeclasses Opaque option_dist.
Arguments optionC : clear implicits.
Instance option_fmap_ne {A B : cofeT} (f : A B) n:
......
......@@ -62,8 +62,8 @@ Proof.
destruct (c 0) as [|x l] eqn:Hc0 at 1.
{ by destruct (chain_cauchy c 0 n); auto with omega. }
rewrite -(λ H, length_ne _ _ _ (chain_cauchy c 0 n H)); last omega.
apply Forall2_lookup=> i; apply dist_option_Forall2.
rewrite list_lookup_fmap. destruct (decide (i < length (c n))); last first.
apply Forall2_lookup=> i. rewrite -dist_option_Forall2 list_lookup_fmap.
destruct (decide (i < length (c n))); last first.
{ rewrite lookup_seq_ge ?lookup_ge_None_2; auto with omega. }
rewrite lookup_seq //= (conv_compl n (list_chain c _ _)) /=.
by destruct (lookup_lt_is_Some_2 (c n) i) as [? ->].
......
......@@ -64,7 +64,7 @@ Proof.
intros (?&?&?). rewrite /ownI; uPred.unseal.
rewrite /uPred_holds/=res_includedN/= singleton_includedN; split.
- intros [(P'&Hi&HP) _]; rewrite Hi.
apply Some_dist, symmetry, agree_valid_includedN; last done.
constructor; symmetry; apply agree_valid_includedN; last done.
by apply lookup_validN_Some with (wld r) i.
- intros ?; split_and?; try apply cmra_unit_leastN; eauto.
Qed.
......
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