gistfile1.txt

(* Is this definition correct? *)
  Definition ltR (u v : R) : bool :=
  match u, v with 
  | Left x, Left y => Nat.ltb x y 
  | Left x, Infinity => true 
  | Infinity, Left _ => false 
  | _, _ => false
  end.

  Definition plusR (u v : R) : R :=
  match u, v with 
  | Left x, Left y => Left (Nat.add x y)
  | _, _ => Infinity 
  end. 

  (* Authors didn't make it clear how infinity in*)
  Definition mulR (u v : R) : R :=
  match u, v with 
  | Left x, Left y => Left (Nat.mul x y)
  | _, _ => Infinity 
  end.


  Definition plusRR (u v : RR) : RR :=
  match u, v with 
  | (au, bu), (av, bv) => 
    match orb (ltR au av) (andb (eqR au av) (ltR bu bv)) with 
    | true => (au, bu)
    | _ => (av, bv)
    end 
  end. 

  Definition minR (u v : R) : R :=
  match u, v with 
  | Left x, Left y => Left (Nat.min x y)
  | Left x, Infinity => Left x
  | Infinity, Left x => Left x 
  | _, _ => Infinity
  end. 


  Definition mulRR (u v : RR) : RR :=
  match u, v with 
  | (au, bu), (av, bv) => (plusR au av, minR bu bv)
  end.  


  Definition finN : list Node := [A; B; C].

  (* Now, configure the matrix *)
  Definition widest_shortest_path (m : Path.Matrix Node RR) : Path.Matrix Node RR :=
    matrix_exp_binary Node eqN finN RR zeroR oneR plusRR mulRR m 2%N.


Theorem refN : brel_reflexive Node eqN. 
  Proof.
    unfold brel_reflexive;
    intros [| | ]; simpl;
    reflexivity.
  Qed.

  Theorem symN : brel_symmetric Node eqN.
  Proof.
    unfold brel_symmetric;
    intros [| | ] [| | ]; simpl;
    try reflexivity; try congruence.
  Qed.

  Theorem trnN : brel_transitive Node eqN.
  Proof.
    unfold brel_transitive;
    intros [| | ] [| | ] [| | ];
    simpl; intros Ha Hb;
    try firstorder. 
  Qed. 


  Theorem dunN : no_dup Node eqN finN = true. 
  Proof.
    reflexivity.
  Qed.

  Theorem lenN : 2 <= List.length finN. 
  Proof.
    cbn; nia. 
  Qed. 

  Theorem memN : ∀ x : Node, in_list eqN finN x = true. 
  Proof.
    intros [| | ];
    cbn; reflexivity.
  Qed.

  Theorem refR : brel_reflexive R eqR.
  Proof.
    unfold brel_reflexive;
    intros [x | ]; cbn;
    [eapply PeanoNat.Nat.eqb_refl | reflexivity].
  Qed. 
  
  Theorem symR : brel_symmetric R eqR.
  Proof.
    unfold brel_symmetric;
    intros [x | ] [y | ]; cbn;
    intros Ha; try reflexivity; 
    try congruence.
    eapply PeanoNat.Nat.eqb_eq in Ha.
    eapply PeanoNat.Nat.eqb_eq. 
    eapply eq_sym; assumption. 
  Qed. 

  Theorem trnR : brel_transitive R eqR.
  Proof.
    unfold brel_transitive;
    intros [x | ] [y | ] [z |]; cbn;
    intros Ha Hb;
    try reflexivity;
    try congruence.
    eapply PeanoNat.Nat.eqb_eq in Ha, Hb.
    eapply PeanoNat.Nat.eqb_eq.
    eapply eq_trans with y;
    try assumption.
  Qed. 

  Declare Scope Mat_scope.
  Delimit Scope Mat_scope with R.
  Bind Scope Mat_scope with R.
  Local Open Scope Mat_scope.

  Local Notation "0" := zeroR : Mat_scope.
  Local Notation "1" := oneR : Mat_scope.
  Local Infix "+" := plusRR : Mat_scope.
  Local Infix "*" := mulRR : Mat_scope.
  Local Infix "=r=" := eqRR (at level 70) : Mat_scope.
  Local Infix "=n=" := eqNN (at level 70) : Mat_scope.


  Theorem zero_left_identity_plus  : forall r : RR, 0 + r =r= r = true.
  Proof.
    intros ([[ | rx] | ], [[|ry] | ]); try reflexivity.
    simpl. admit.