Bivalent with lights compiles without (unwanted) axioms!

CaseStudies/Gathering/InR2/Algorithm_withLight_Assumptions.v

+Require Pactole.CaseStudies.Gathering.InR2.Algorithm_withLight.
+Print Assumptions InR2.Algorithm_withLight.Gathering_in_R2.

CaseStudies/Gathering/WithMultiplicityLight.v

@@ -1409,8 +1409,52 @@ Qed.
 Lemma color_bivalent_correct : forall config st,
   color_bivalent_obs (obs_from_config config st) = true -> color_bivalent config.
 Proof using .
-(* TODO *)
-Admitted.
+  intros config st h_bivobs. 
+  specialize (color_bivalent_obs_bivalent_obs _ h_bivobs) as h_biv.
+  rewrite bivalent_obs_spec in h_biv.
+  red in h_biv.
+  destruct h_biv as [heq_n [h_lt_n _]].
+  revert h_bivobs.
+  unfold color_bivalent, color_bivalent_obs.
+  repeat (destruct_match; subst; try discriminate).
+  intros h_and.
+  split;auto.
+  split;auto.
+
+  apply andb_prop in h_and.
+  destruct h_and as [ heq_loc h_forall].
+  apply Nat.eqb_eq in heq_loc.
+  rewrite  forallb_forall in h_forall.
+  setoid_rewrite Nat.eqb_eq in h_forall.
+  
+  specialize (obs_from_config_fst_spec config (origin,witness)) as h.
+  specialize (h l) as h_l.
+  specialize (h l1) as h_l1.
+  clear h.
+  specialize (cardinal_fst_obs_from_config config (origin,witness)) as h_cardinal.
+  rewrite <- obs_fst in *.
+  rewrite cardinal_fold_support in h_cardinal.
+  rewrite <- obs_from_config_fst_ok with (st:=(0%VS, witness)) in H.
+  rewrite H in h_cardinal.
+  cbn in h_cardinal.
+  rewrite Nat.add_0_r in h_cardinal.
+  specialize (support_NoDupA (!! config)) as h.
+  rewrite H in h.
+  apply NoDupA_2 in h.
+  exists l, l1.
+  split;auto.
+  rewrite heq_loc in h_cardinal.
+  match type of h_cardinal with
+    ?A + ?A = ?B => replace (A + A) with (2 * A) in h_cardinal
+  end.
+  2:{ lia. }
+  rewrite <- h_cardinal.
+  rewrite Nat.div2_double.
+  rewrite Forall_forall.
+  repeat split;auto.
+Qed.
+
+
 
 Lemma color_bivalent_complete : forall config st,
   color_bivalent config -> color_bivalent_obs (obs_from_config config st) = true.

_CoqProject

@@ -108,6 +108,7 @@ CaseStudies/Gathering/InR2/Peleg_Assumptions.v
 CaseStudies/Gathering/InR2/Viglietta.v
 CaseStudies/Gathering/InR2/Viglietta_Assumptions.v
 CaseStudies/Gathering/InR2/Algorithm_withLight.v
+CaseStudies/Gathering/InR2/Algorithm_withLight_Assumptions.v
 
 
 ## Case Study: Ring Exploration