proposition: Lemma eval_mem_cap (a: Atom) e: e ⊓ atom a ≡ if eval (set.mem a) e then atom a else bot with eval_mem_cup (a: Atom) e: e ⊔ !atom a ≡ if eval (set.mem a) e then top else !atom a.
proof: Proof. - destruct e; simpl eval. apply capbx. apply captx. rewrite capC, capcup, capC, eval_mem_cap, capC, eval_mem_cap. case (eval (set.mem a) e1); case (eval (set.mem a) e2); lattice. transitivity ((e1 ⊓ atom a) ⊓ (e2 ⊓ atom a)). lattice. rewrite 2eval_mem_cap. case (eval (set.mem a) e1); case (eval (set.mem a) e2); lattice. neg_switch. rewrite negcap, negneg, eval_mem_cup. case (eval (set.mem a) e). now rewrite <-negbot. reflexivity. apply cap_var_atom. - destruct e; simpl eval. apply cupbx. apply cuptx. transitivity ((e1 ⊔ !atom a) ⊔ (e2 ⊔ !atom a)). lattice. rewrite 2eval_mem_cup. case (eval (set.mem a) e1); case (eval (set.mem a) e2); lattice. rewrite cupC, cupcap, cupC, eval_mem_cup, cupC, eval_mem_cup. case (eval (set.mem a) e1); case (eval (set.mem a) e2); lattice. neg_switch. rewrite negcup, 2negneg, eval_mem_cap. case (eval (set.mem a) e). apply negneg. apply negtop. apply cup_var_atom. Qed.
imports: lattice lsyntax comparisons lset boolean sups