Skip to content

Add lemmas for validity of `●{_} _ ⋅ ●{_} _` for both view and auth.

Robbert Krebbers requested to merge robbert/auth_valid into master

The diff might be hard to read, because I had to change the order. The following lemmas have been added:

Lemma view_auth_frac_op_validN n q1 q2 a1 a2 :
  {n} (V{q1} a1  V{q2} a2)   (q1 + q2)%Qp  a1 {n} a2  rel n a1 ε.
Lemma view_auth_op_validN n a1 a2 : {n} (V a1  V a2)  False.

Lemma view_auth_frac_op_valid q1 q2 a1 a2 :
   (V{q1} a1  V{q2} a2)   (q1 + q2)%Qp  a1  a2   n, rel n a1 ε.
Lemma view_auth_op_valid a1 a2 :  (V a1  V a2)  False.

Lemma auth_auth_frac_op_validN n q1 q2 a1 a2 :
  {n} ({q1} a1  {q2} a2)   (q1 + q2)%Qp  a1 {n} a2  {n} a1.
Lemma auth_auth_op_validN n a1 a2 : {n} ( a1   a2)  False.

Lemma auth_auth_frac_op_valid q1 q2 a1 a2 :
   ({q1} a1  {q2} a2)   (q1 + q2)%Qp  a1  a2   a1.
Lemma auth_auth_op_valid a1 a2 :  ( a1   a2)  False.

Merge request reports