proposition: Lemma lift_brelation_iff_false_elements {A} (R : A -> A -> bool) (default : A) (m1 m2 : t A) (elms := (elements (map2 (fun x1 x2 => match x1, x2 with | Some x1, Some x2 => Some (R x1 x2) | Some x, None => Some (R x default) | None, Some x => Some (R default x) | None, None => None end) m1 m2))) : lift_brelation R default m1 m2 = false <-> (exists x, InA (@eq_key_elt _) x elms /\ snd x = false).
proof: Proof. unfold lift_brelation, lift_brelation_hetero, lift_relation_gen_hetero; FMap_convert. setoid_rewrite InA_alt. subst elms. let ls := match goal with |- context[elements ?m] => constr:(elements m) end in induction ls as [|x xs IHxs]. { simpl. split; intro H; [ exfalso; apply H | ]; repeat intuition (tauto || congruence || simpl in * || destruct_head ex || eauto). } { simpl. setoid_rewrite_logic. setoid_rewrite <- IHxs; clear IHxs. setoid_rewrite <- InA_alt. repeat setoid_rewrite (and_comm _ (_ = _)). setoid_rewrite_logic. destruct x as [k []]; simpl; setoid_rewrite_logic. { reflexivity. } { setoid_rewrite (True_iff (ex_intro (fun y => E.eq y k) k (reflexivity _))). setoid_rewrite (forall_iff_nondep (ex_intro (fun y => E.eq y k) k (reflexivity _))). tauto. } } 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