congruence.v

Lemma constructive_deci : forall (c d : cand) (k : nat),
      {constructive_prop c d k} + {~(constructive_prop c d k)}.
  Proof.
    intros c d k. unfold constructive_prop.
    remember (all_pairs cand_all) as v.
    destruct (bool_dec ((Fixpoints.iter (O k) (length v) (fun _  => false)) (c, d)) true) as [H | H].
    left. split. apply path_lfp. unfold Fixpoints.least_fixed_point. unfold Fixpoints.empty_ss.
    rewrite <- Heqv. assumption.
    intros l Hl. apply path_lfp in Hl.
    unfold Fixpoints.least_fixed_point in Hl. unfold Fixpoints.empty_ss in Hl.
    rewrite <- Heqv in Hl.
    (* admit it for the moment *)
    admit.
    apply not_true_is_false in H.
    right. intros [Hk Hl]. apply path_lfp in Hk. 
    unfold Fixpoints.least_fixed_point, Fixpoints.empty_ss in Hk.
    rewrite <- Heqv in Hk.




  
  
  
  c, d : cand
  k : nat
  v : list (cand * cand)
  Heqv : v = all_pairs cand_all
  H : Fixpoints.iter (O k) (length v) (fun _ : cand * cand => false) (c, d) = false
  Hk : Fixpoints.iter (O k) (length v) (fun _ : cand * cand => false) (c, d) = true
  Hl : forall l : nat, Path l d c -> l <= k
  ============================
  False

Complete source code
https://github.com/mukeshtiwari/formalized-voting/blob/master/Schulze_Dirk.v#L680