proposition: Lemma lift_brelation_iff_false {A} (R : A -> A -> bool) (default : A) (m1 m2 : t A) : lift_brelation R default m1 m2 = false <-> exists k, match find k m1, find k m2 return bool with | Some x1, Some x2 => negb (R x1 x2) | Some x, None => negb (R x default) | None, Some x => negb (R default x) | None, None => false end.
proof: Proof. rewrite lift_brelation_iff_false_elements. FMap_convert_to_find. split; [ intros [[k v] H]; exists k; simpl in * | intros [k H]; exists (k, false); split; simpl in *; [ | congruence ] ]; do 2 edestruct find; repeat match goal with | [ H : and _ _ |- _ ] => destruct H | [ H : _ <> true |- _ ] => apply not_true_iff_false in H | _ => progress subst | _ => setoid_rewrite negb_true_iff | [ H : context[negb _] |- _ ] => setoid_rewrite negb_true_iff in H | _ => congruence end. Qed.
imports: Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.Program.Program Coq.Structures.OrderedTypeEx Fiat.Common Fiat.Common.SetEq Fiat.Common.SetEqProperties Fiat.Common.List.ListFacts Fiat.Common.List.ListMorphisms Fiat.Common.LogicFacts Fiat.Common.SetoidClassInstances