diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/graphs/cgraph.v | 2744 | ||||
| -rw-r--r-- | contrib/graphs/zcgraph.v | 417 |
2 files changed, 3161 insertions, 0 deletions
diff --git a/contrib/graphs/cgraph.v b/contrib/graphs/cgraph.v new file mode 100644 index 000000000..3f7203339 --- /dev/null +++ b/contrib/graphs/cgraph.v @@ -0,0 +1,2744 @@ + +(*s Decision procedure for arithmetic formulas by looking + for negative cycles in a graph *) + +Require Allmaps. +Require Arith. +Require ZArith. +Require Bool. +Require Sumbool. +Require PolyList. +Require Wf_nat. + +Section ConstraintGraphs. + +(*s Axiomatisation of the domain of interpretation [D] *) + + Variable D : Set. + + Variable Dz : D. + Variable Dplus : D -> D -> D. + Variable Dneg : D -> D. + Variable Dle : D -> D -> bool. + + Variable Dplus_d_z : (d:D) (Dplus d Dz)=d. + Variable Dplus_z_d : (d:D) (Dplus Dz d)=d. + Variable Dplus_assoc : + (d,d',d'':D) (Dplus (Dplus d d') d'')=(Dplus d (Dplus d' d'')). + + Variable Dplus_neg : (d:D) (Dplus d (Dneg d))=Dz. + + Variable Dle_refl : (d:D) (Dle d d)=true. + Variable Dle_antisym : (d,d':D) (Dle d d')=true -> (Dle d' d)=true -> d=d'. + Variable Dle_trans : + (d,d',d'':D) (Dle d d')=true -> (Dle d' d'')=true -> (Dle d d'')=true. + Variable Dle_total : (d,d':D) {(Dle d d')=true}+{(Dle d' d)=true}. + + Variable Dle_plus_mono : + (d,d',d'',d''':D) (Dle d d')=true -> (Dle d'' d''')=true -> + (Dle (Dplus d d'') (Dplus d' d'''))=true. + +(*s Properties of [Dle] *) + +Lemma Dle_true_permut : + (d,d':D) (Dle d d')=true -> {(Dle d' d)=false}+{d=d'}. + Intros; Case (sumbool_of_bool (Dle d' d)); Intro; Auto. + Save. + +(*s Definition of the minimum function *) + +Definition Dmin := [d,d':D] if (Dle d d') then d else d'. + +Lemma Dle_true_Dmin : (d,d':D)(Dle d d')=true -> (Dmin d d')=d. + Unfold Dmin; Intros d d' H; Rewrite H; Trivial. + Save. + +Lemma Dle_inv_Dmin : (d,d':D)(Dle d' d)=true -> (Dmin d d')=d'. + Unfold Dmin; Intros d d' H. + Case (sumbool_of_bool (Dle d d')); Intro H'; Rewrite H'; Auto. + Save. + +Hints Resolve Dle_true_Dmin Dle_inv_Dmin. + +Lemma Dmin_idempotent : (d:D) (Dmin d d)=d. + Proof. + Auto. + Qed. + +Lemma Dmin_comm : (d,d':D) (Dmin d d')=(Dmin d' d). + Proof. + Intros d d'; Case (Dle_total d d'); Intro H. + Rewrite Dle_true_Dmin with 1:= H. + Rewrite Dle_inv_Dmin with 1:= H; Trivial. + Rewrite Dle_true_Dmin with 1:= H. + Rewrite Dle_inv_Dmin with 1:= H; Trivial. + Save. + +Lemma Dmin_assoc + : (d,d',d'':D) (Dmin (Dmin d d') d'')=(Dmin d (Dmin d' d'')). + Proof. + Intros d d' d''; Case (Dle_total d d'); Intro H. + Rewrite Dle_true_Dmin with 1:= H. + Case (Dle_total d' d''); Intro H'. + Rewrite Dle_true_Dmin with 1:= H'. + Rewrite Dle_true_Dmin with 1:= H. + Rewrite (Dle_true_Dmin d d''); EAuto. + Rewrite Dle_inv_Dmin with 1:= H'; Trivial. + Rewrite Dle_inv_Dmin with 1:= H. + Case (Dle_total d' d''); Intro H'. + Rewrite Dle_true_Dmin with 1:= H'. + Rewrite Dle_inv_Dmin with 1:= H; Trivial. + Rewrite Dle_inv_Dmin with 1:= H'. + Rewrite (Dle_inv_Dmin d d''); EAuto. +Save. + +Lemma Dmin_le_1 : (d,d':D) (Dle (Dmin d d') d)=true. + Proof. + Intros. Case (Dle_total d d'); Intro H. + Rewrite Dle_true_Dmin with 1:= H; Auto. + Rewrite Dle_inv_Dmin with 1:= H; Auto. + Qed. + +Lemma Dmin_le_2 : (d,d':D) (Dle (Dmin d d') d')=true. + Proof. + Intros. Rewrite (Dmin_comm d d'). Apply Dmin_le_1. + Qed. + +Lemma Dmin_le_3 : (d,d',d'':D) (Dle d (Dmin d' d''))=true -> (Dle d d')=true. + Proof. + Intros d d' d''; Elim (Dle_total d' d''); Intro H0. + Rewrite Dle_true_Dmin with 1:=H0; Trivial. + Rewrite Dle_inv_Dmin with 1:=H0; EAuto. + Qed. + +Lemma Dmin_le_4 : (d,d',d'':D) (Dle d (Dmin d' d''))=true -> (Dle d d'')=true. + Proof. + Intros. Rewrite (Dmin_comm d' d'') in H. Exact (Dmin_le_3 ? ? ? H). + Qed. + +Lemma Dmin_le_5 : (d,d',d'':D) (Dle d d')=true -> (Dle d d'')=true -> + (Dle d (Dmin d' d''))=true. + Proof. + Intros. Unfold Dmin. Case (Dle d' d''); Assumption. + Qed. + +(*s Properties of [Dneg] *) + +Lemma Dneg_Dz : (Dneg Dz)=Dz. + Proof. + Rewrite <- (Dplus_z_d (Dneg Dz)). Apply Dplus_neg. + Qed. + +Lemma Dneg_neg : (d:D) (Dneg (Dneg d))=d. + Proof. + Intro. Rewrite <- (Dplus_z_d (Dneg (Dneg d))). Rewrite <- (Dplus_neg d). + Rewrite Dplus_assoc. Rewrite Dplus_neg. Apply Dplus_d_z. + Qed. + +Lemma Dplus_neg_2 : (d:D) (Dplus (Dneg d) d)=Dz. + Proof. + Intro. Cut (Dplus (Dneg d) (Dneg (Dneg d)))=Dz. Rewrite Dneg_neg. Trivial. + Apply Dplus_neg. + Qed. + +(*s Properties of [Dplus] *) + +Lemma Dplus_reg_l + : (d,d',d'':D) (Dle (Dplus d'' d) (Dplus d'' d'))=true + -> (Dle d d')=true. + Proof. + Intros. Rewrite <- (Dplus_z_d d). Rewrite <- (Dplus_z_d d'). Rewrite <- (Dplus_neg_2 d''). + Rewrite (Dplus_assoc (Dneg d'') d'' d). Rewrite (Dplus_assoc (Dneg d'') d'' d'). + Apply Dle_plus_mono. Apply Dle_refl. + Assumption. + Qed. + +Lemma Dplus_reg_r + : (d,d',d'':D) (Dle (Dplus d d'') (Dplus d' d''))=true -> (Dle d d')=true. + Proof. + Intros. Rewrite <- (Dplus_d_z d). Rewrite <- (Dplus_d_z d'). Rewrite <- (Dplus_neg d''). + Rewrite <- (Dplus_assoc d d'' (Dneg d'')). Rewrite <- (Dplus_assoc d' d'' (Dneg d'')). + Apply Dle_plus_mono. Assumption. + Apply Dle_refl. + Qed. + +Lemma Dmin_plus_l + : (d,d',d'':D) (Dplus (Dmin d d') d'')=(Dmin (Dplus d d'') (Dplus d' d'')). + Proof. + Intros d d' d''; Case (Dle_total d d'); Intro H. + Rewrite Dle_true_Dmin with 1:=H. + Rewrite (Dle_true_Dmin (Dplus d d'')); Auto. + Rewrite Dle_inv_Dmin with 1:=H. + Rewrite (Dle_inv_Dmin (Dplus d d'')); Auto. + Qed. + +Lemma Dmin_plus_r + : (d,d',d'':D) (Dplus d'' (Dmin d d'))=(Dmin (Dplus d'' d) (Dplus d'' d')). + Proof. + Intros d d' d''; Case (Dle_total d d'); Intro H. + Rewrite Dle_true_Dmin with 1:=H. + Rewrite (Dle_true_Dmin (Dplus d'' d)); Auto. + Rewrite Dle_inv_Dmin with 1:=H. + Rewrite (Dle_inv_Dmin (Dplus d'' d)); Auto. + Qed. + +Lemma Dle_neg : (d:D) (Dle Dz d)=true -> (Dle (Dneg d) Dz)=true. + Proof. + Intros. Cut (Dle (Dplus Dz (Dneg d)) (Dplus d (Dneg d)))=true. Intro. + Rewrite (Dplus_z_d (Dneg d)) in H0. Rewrite (Dplus_neg d) in H0. Assumption. + Exact (Dle_plus_mono ? ? ? ? H (Dle_refl ?)). + Qed. + +Lemma Dle_neg_2 : (d:D) (Dle d Dz)=true -> (Dle Dz (Dneg d))=true. + Proof. + Intros. Cut (Dle (Dplus d (Dneg d)) (Dplus Dz (Dneg d)))=true. Intro. + Rewrite (Dplus_neg d) in H0. Rewrite (Dplus_z_d (Dneg d)) in H0. Assumption. + Exact (Dle_plus_mono ? ? ? ? H (Dle_refl ?)). + Qed. + +Lemma Dnotle_not_eq : (d,d':D)(Dle d d')=false ->~d=d'. + Red; Intros. + Apply diff_true_false. + Rewrite H0 in H. + Rewrite (Dle_refl d') in H; Trivial. + Save. + +Hints Immediate Dnotle_not_eq. + +Lemma Dnotle_not_eq_sym : (d,d':D) (Dle d d')=false -> ~d'=d. + Proof. + Intros; Apply sym_not_eq; Auto. + Qed. + +Hints Immediate Dnotle_not_eq_sym. + +(*s Equality on [D] is decidable *) + +Lemma D_dec : (d,d':D) {d=d'}+{~d=d'}. + Proof. + Intros d d'; Case (sumbool_of_bool (Dle d d')); Intro H; Auto. + Case (sumbool_of_bool (Dle d' d)); Intro H0; Auto. + Qed. + +Lemma Dnotle_3_cases + : (d,d':D) {(Dle d d')=false}+{d=d'}+{(Dle d' d)=false}. + Proof. + Intros d d'; Case (sumbool_of_bool (Dle d d')); Intro H; Auto. + Case (sumbool_of_bool (Dle d' d)); Intro H0; Auto. + Qed. + +Lemma Dle_noteq_notle + : (d,d':D) (Dle d' d)=true -> ~d=d' -> (Dle d d')=false. + Proof. + Intros d d'; Case (sumbool_of_bool (Dle d d')); Intro H; Auto. + Intros; Absurd d=d'; Auto. + Qed. + +Lemma Dnotle_not_refl + : (d:D) ~(Dle d d)=false. + Proof. + Red; Intro; Rewrite (Dle_refl d). + Exact diff_true_false. + Qed. + + +Lemma Dnotle_elim : + (d,d':D) (Dle d' d)=false -> ((Dle d d')=true /\ ~d=d'). + Intros. + Case (Dle_total d d'); Intro H'; Auto. + Case diff_true_false. + Rewrite <- H'; Trivial. +Save. + +Lemma Dnotle_trans : (d,d',d'':D) (Dle d d')=false -> (Dle d' d'')=false -> (Dle d d'')=false. + Proof. + Intros. + Case Dnotle_elim with 1:= H; Intros. + Case Dnotle_elim with 1:= H0; Intros. + Apply Dle_noteq_notle; EAuto. + Red; Intros. + Apply diff_false_true. + Rewrite <- H0. + Rewrite <- H5; Trivial. + Save. + +Lemma Dnotle_le_1 : (d,d':D) (Dle d d')=false -> (Dle d' d)=true. + Proof. + Intros; Case Dnotle_elim with 1:= H; Trivial. + Qed. + +Lemma Dmin_le_distr_l : (d,d',d'':D) (Dle (Dmin d d') d'')=(orb (Dle d d'') (Dle d' d'')). + Proof. + Intros; Case (Dle_total d d'); Intro H. + Rewrite Dle_true_Dmin with 1:= H. + Pattern (Dle d d''); Apply bool_eq_ind; Intro H'; Simpl; Trivial. + Pattern (Dle d' d''); Apply bool_eq_ind; Intro H''; Simpl; Trivial. + Rewrite <- H'; EAuto. + Rewrite Dle_inv_Dmin with 1:= H. + Pattern (Dle d d''); Apply bool_eq_ind; Intro H'; Simpl; EAuto. + Save. + +Lemma Dmin_choice : (d,d':D) {(Dmin d d')=d}+{(Dmin d d')=d'}. + Proof. + Unfold Dmin. Intros. Elim (sumbool_of_bool (Dle d d')). Intro H. Left . Rewrite H. Reflexivity. + Intro H. Right . Rewrite H. Reflexivity. + Qed. + +Lemma Dnotle_noteq : (d,d':D) (Dle d d')=false -> ~d=d'. + Proof. + Unfold not. Intros. Rewrite H0 in H. Rewrite (Dle_refl d') in H. Discriminate H. + Qed. + +Lemma Dneg_plus : (d,d':D) (Dneg (Dplus d d'))=(Dplus (Dneg d') (Dneg d)). + Proof. + Intros. Cut (Dplus (Dplus d d') (Dplus (Dneg d') (Dneg d)))=Dz. Intro. + Rewrite <- (Dplus_d_z (Dneg (Dplus d d'))). Rewrite <- H. Rewrite <- Dplus_assoc. + Rewrite Dplus_neg_2. Rewrite Dplus_z_d. Reflexivity. + Rewrite Dplus_assoc. Rewrite <- (Dplus_assoc d' (Dneg d') (Dneg d)). Rewrite Dplus_neg. + Rewrite Dplus_z_d. Apply Dplus_neg. + Qed. + +Lemma Dneg_le : (d,d':D) (Dle d d')=true -> (Dle (Dneg d') (Dneg d))=true. + Proof. + Intros. Apply Dplus_reg_l with d'':=d'. Rewrite Dplus_neg. Rewrite <- (Dneg_neg d'). + Rewrite <- Dneg_plus. Apply Dle_neg_2. Rewrite <- (Dplus_neg d'). + Exact (Dle_plus_mono ? ? ? ? H (Dle_refl ?)). + Qed. + +Lemma Dnotle_plus_mono_1 : (d,d',d'',d''':D) (Dle d' d)=true -> (Dle d'' d''')=false + -> (Dle (Dplus d d'') (Dplus d' d'''))=false. + Proof. + Intros. Apply Dle_noteq_notle. Apply Dle_plus_mono. Assumption. + Apply Dnotle_le_1. Assumption. + Unfold not. Intro H1. + Cut (Dle (Dplus (Dneg d) (Dplus d d'')) (Dplus (Dneg d') (Dplus d' d''')))=true. + Rewrite <- (Dplus_assoc (Dneg d) d d''). Rewrite Dplus_neg_2. Rewrite Dplus_z_d. + Rewrite <- Dplus_assoc. Rewrite Dplus_neg_2. Rewrite Dplus_z_d. Rewrite H0. + Intro H2. Discriminate H2. + Apply Dle_plus_mono. Apply Dneg_le. Assumption. + Rewrite H1. Apply Dle_refl. + Qed. + +Lemma Dnotle_plus_mono : (d,d',d'',d''':D) (Dle d d')=false -> (Dle d'' d''')=false + -> (Dle (Dplus d d'') (Dplus d' d'''))=false. + Proof. + Intros. (Apply Dnotle_plus_mono_1; Try Assumption). (Apply Dnotle_le_1; Assumption). + Qed. + +(*s Extending D with an element NONE representing infinity *) + +Definition Ddmin := [dd,dd':(option D)] Cases dd dd' of + NONE _ => dd' + | _ NONE => dd + | (SOME d) (SOME d') => (SOME D (Dmin d d')) + end. + +Lemma Ddmin_idempotent : (dd:(option D)) (Ddmin dd dd)=dd. + Proof. + Induction dd. Trivial. + Intro. Simpl. Rewrite Dmin_idempotent. Reflexivity. + Qed. + +Lemma Ddmin_comm : (dd,dd':(option D)) (Ddmin dd dd')=(Ddmin dd' dd). + Proof. + Induction dd. Intro. (Case dd'; Reflexivity). + Intro d. Induction dd'. Reflexivity. + Intro d'. Simpl. Rewrite Dmin_comm. Reflexivity. + Qed. + +Lemma Ddmin_assoc : (dd,dd',dd'':(option D)) + (Ddmin (Ddmin dd dd') dd'')=(Ddmin dd (Ddmin dd' dd'')). + Proof. + Intros. Case dd. Simpl. Case dd'. Simpl. (Case dd''; Reflexivity). + Intro. Simpl. (Case dd''; Reflexivity). + Intro. Simpl. Case dd'. Simpl. (Case dd''; Reflexivity). + Intro d'. Simpl. Case dd''. Reflexivity. + Intro d''. Rewrite Dmin_assoc. Reflexivity. + Qed. + +(*s The order [Dle] extended to $D_{\infty}$ *) +Definition Ddle + := [dd,dd':(option D)] Cases dd dd' of + _ NONE => true + | NONE _ => false + | (SOME d) (SOME d') => (Dle d d') + end. + +Lemma Ddle_refl : (dd:(option D)) (Ddle dd dd)=true. + Proof. + Intro. Case dd. Reflexivity. + Intro. Exact (Dle_refl d). + Qed. + +Lemma Ddle_antisym + : (dd,dd':(option D)) (Ddle dd dd')=true -> (Ddle dd' dd)=true -> dd=dd'. + Proof. + Intros dd dd'. Case dd. Case dd'. Trivial. + Intros. Discriminate H. + Case dd'. Intros. Discriminate H0. + Intros. Rewrite (Dle_antisym ? ? H0 H). Reflexivity. + Qed. + +Lemma Ddle_trans + : (dd,dd',dd'':(option D)) + (Ddle dd dd')=true -> (Ddle dd' dd'')=true -> (Ddle dd dd'')=true. + Proof. + Intros dd dd' dd''. Case dd''. (Case dd; Trivial). + Intro d''. Case dd'. Intros. Discriminate H0. + Intro d'. Case dd. Intro. Discriminate H. + Intros d H H0. Exact (Dle_trans ? ? ? H H0). + Qed. + +Lemma Ddle_d_none : (dd:(option D)) (Ddle dd (NONE D))=true. + Proof. + Induction dd; Trivial. + Qed. + +Lemma Ddmin_le_1 : (dd,dd':(option D)) (Ddle (Ddmin dd dd') dd)=true. + Proof. + Intros. Case dd. (Case dd'; Reflexivity). + Intro d. Case dd'. Apply Ddle_refl. + Exact (Dmin_le_1 d). + Qed. + +Lemma Ddmin_le_2 : (dd,dd':(option D)) (Ddle (Ddmin dd dd') dd')=true. + Proof. + Intros. Rewrite (Ddmin_comm dd dd'). Apply Ddmin_le_1. + Qed. + +Lemma Ddmin_le_3 + : (dd,dd',dd'':(option D)) + (Ddle dd (Ddmin dd' dd''))=true -> (Ddle dd dd')=true. + Proof. + Intros dd dd' dd''. Case dd'. (Case dd; Trivial). + Intro d'. Case dd. Case dd''. Intro. Discriminate H. + Intros d'' H. Discriminate H. + Intro d. Case dd''. Trivial. + Exact (Dmin_le_3 d d'). + Qed. + +Lemma Ddmin_le_4 : (dd,dd',dd'':(option D)) (Ddle dd (Ddmin dd' dd''))=true -> + (Ddle dd dd'')=true. + Proof. + Intros. Rewrite (Ddmin_comm dd' dd'') in H. Exact (Ddmin_le_3 ? ? ? H). + Qed. + +Lemma Ddmin_le_distr_l + : (dd,dd',dd'':(option D)) + (Ddle (Ddmin dd dd') dd'')=(orb (Ddle dd dd'') (Ddle dd' dd'')). + Proof. + Induction dd. Induction dd'. (Induction dd''; Trivial). + Intro d. (Induction dd''; Trivial). + Intro d. Induction dd'. (Induction dd''; Trivial). + Simpl. Intro d'. Rewrite orb_b_false. Reflexivity. + Intro d'. (Induction dd''; Trivial). Simpl. Exact (Dmin_le_distr_l d d'). + Qed. + +Lemma Ddmin_choice + : (dd,dd':(option D)) {(Ddmin dd dd')=dd}+{(Ddmin dd dd')=dd'}. + Proof. + Induction dd. Intro. Right . Simpl. (Case dd'; Reflexivity). + Intro d. Induction dd'. Left . Reflexivity. + Intro d'. Simpl. Elim (Dmin_choice d d'). Intro H. Left . Rewrite H. Reflexivity. + Intro H. Right . Rewrite H. Reflexivity. + Qed. + +(*s Operation [Ddplus] on $D_{\infty}$ *) + +Definition Ddplus := [dd:(option D)][d':D] + Cases dd of + (SOME d) => (SOME ? (Dplus d d')) + | _ => dd + end. + +Lemma Ddmin_plus_l + : (dd,dd':(option D)) (d'':D) + (Ddplus (Ddmin dd dd') d'')=(Ddmin (Ddplus dd d'') (Ddplus dd' d'')). + Proof. + Induction dd. Induction dd'. Trivial. + Trivial. + Intro d. Induction dd'. Trivial. + Intros d' d''. Simpl. Rewrite Dmin_plus_l. Reflexivity. + Qed. + +Lemma Ddle_plus_mono + : (dd,dd':(option D)) (d,d':D) + (Ddle dd dd')=true -> (Dle d d')=true -> + (Ddle (Ddplus dd d) (Ddplus dd' d'))=true. + Proof. + Induction dd. Induction dd'. Intros. Trivial. + Simpl. Intros. Assumption. + Intro d0. Induction dd'. Trivial. + Simpl. Exact (Dle_plus_mono d0). + Qed. + +Lemma Ddplus_reg_r + : (dd,dd':(option D)) (d'':D) + (Ddle (Ddplus dd d'') (Ddplus dd' d''))=true->(Ddle dd dd')=true. + Proof. + Induction dd. Induction dd'. Trivial. + Simpl. Trivial. + Intro d. Induction dd'. Trivial. + Intros d' d'' H. Exact (Dplus_reg_r d d' d'' H). + Qed. + +(*s Introducing graphs of objects in [D] *) + +Definition CGraph1 := (Map (Map D)). + +Definition CGraph := (option CGraph1). + +Section CGDist. + + Variable cg : CGraph1. + +Definition CG_edge := [x,y:ad] + Cases (MapGet ? cg x) of + (SOME edges) => Cases (MapGet ? edges y) of + (SOME d) => (SOME D d) + | _ => (NONE D) + end + | _ => (NONE D) + end. + +(*s Let $\rho$ be an interpretation of adresses as elements in [D], + the graph [cg] is satisfied by $\rho$ if for any edge + from $x$ to $y$ indexed by $d$, we have $\rho(x) \leq \rho(y)+d$ + A graph is consistent if there exists an interpretation which satisfies it. +*) + +Definition CGsat + := [rho:ad->D] + (x,y:ad) (d:D) + (CG_edge x y)=(SOME D d) -> (Dle (rho x) (Dplus (rho y) d))=true. + + +Definition CGconsistent := (sig ? CGsat). + +(* [CG_path last d l] if there exists a path starting from [last] with successive + vertexes $l=[x0;...;xn]$ $(xn=last)$ and [d] is the sum of the weights on the + edges *) + +Inductive CG_path [last : ad] : D -> (list ad) -> Set := + CG_p1 : (x:ad) x=last -> (CG_path last Dz (cons x (nil ?))) + | CG_p2 : (x,y:ad) (l:(list ad)) (d:D) (CG_path last d (cons y l)) -> + (d':D) (CG_edge x y)=(SOME D d') -> + (CG_path last (Dplus d d') (cons x (cons y l))). + +(* If $\rho$ satisfies the graph and there is a path from [last] to [x] of + weight d then $\rho(x) \leq \rho(last)+d$ +*) + +Definition first : (list ad) -> ad := [l]Cases l of nil => ad_z | (cons x _) => x end. + +Lemma CG_path_head + : (l:(list ad)) (last:ad) (d:D) (CG_path last d l) -> + (rho:ad->D) (CGsat rho) -> (Dle (rho (first l)) (Dplus (rho last) d))=true. + Proof. + Intros; Elim H; Simpl; Intros. + Rewrite e; Rewrite Dplus_d_z; Auto. + Apply Dle_trans with (Dplus (rho y) d'); Auto. + Rewrite <- Dplus_assoc; Auto. + Save. + +Lemma CG_path_correct + : (l:(list ad)) (x,last:ad) (d:D) (CG_path last d (cons x l)) -> + (rho:ad->D) (CGsat rho) -> (Dle (rho x) (Dplus (rho last) d))=true. + Proof. + Intros; Apply (CG_path_head (cons x l) last d); Trivial. + Save. + +(*s If there is a circuit [(cons x l)] with negative weight [d], then [cg] is inconsistent: *) + +Theorem CG_circuit_correct + : (x:ad) (d:D) (l:(list ad)) + (CG_path x d (cons x l)) -> (Dle Dz d)=false -> CGconsistent -> False. + Proof. + Intros. Unfold CGconsistent in H1. Elim H1. Intros rho H2. + Cut (Dle (Dplus (rho x) Dz) (Dplus (rho x) d))=true. Intro H3. + Rewrite (Dplus_reg_l ? ? ? H3) in H0. Discriminate H0. + Rewrite Dplus_d_z. Exact (CG_path_correct l x x d H rho H2). + Qed. + +Section CGConsistent. + + Variable P : CGconsistent. + +(*s Assuming that [cg] is consistent, we can build a distance d(x,y) as follows: + d(x,y) is the length of the shortest path from x to y (or +infty if none). *) + +Lemma CG_circuits_non_negative_weight + : (x:ad) (d:D) (l:(list ad)) (CG_path x d (cons x l)) -> (Dle Dz d)=true. + Proof. + Intros. Elim (sumbool_of_bool (Dle Dz d)). Trivial. + Intro H0. Elim (CG_circuit_correct x d l H H0 P). + Qed. + +End CGConsistent. + +(*s We assume that any cycle has a positive weight *) + +Section CGNoBadCycles. + + Variable no_bad_cycles : (x:ad) (d:D) (l:(list ad)) + (CG_path x d (cons x l)) -> (Dle Dz d)=true. + +(*s The edges are in the domain of the graph *) + +Lemma CG_edge_in_cg_1 + : (x,y:ad) (d:D) (CG_edge x y)=(SOME D d) -> (in_FSet x (MapDom ? cg))=true. + Proof. + Unfold CG_edge. Intros x y d. + Elim (option_sum ? (MapGet (Map D) cg x)). Intro H. + Elim H. Intros edges H0. Rewrite H0. Intros. + Exact (MapDom_semantics_1 ? cg x edges H0). + Intros H H0. Rewrite H in H0. Discriminate H0. + Qed. + + +(*s The elements of a path are in the domain of the graph extended with + the last element *) +Lemma CG_path_in_cg_1 + : (l:(list ad)) (last:ad) (d:D) + (CG_path last d l) -> (MapSubset ? ? (Elems l) + (MapPut ? (MapDom ? cg) last tt)). + Proof. + + Induction 1. + Unfold MapSubset; Unfold Elems; Simpl; Intros. + Rewrite in_dom_put. + Rewrite in_dom_M1 in H0. + Rewrite <- e. + Rewrite (ad_eq_comm a x). + Rewrite H0; Simpl; Trivial. + Unfold MapSubset. + Intros; Rewrite in_dom_put. + Change (in_dom unit a + (MapPut unit (Elems (cons y l0)) x tt))=true in H1. + Rewrite in_dom_put in H1. + Case orb_prop with 1:=H1; Intro. + Rewrite (ad_eq_complete ? ? H2). + Change + (orb (ad_eq x last) (in_FSet x (MapDom (Map D) cg)))=true. + Rewrite CG_edge_in_cg_1 with 1:=e; Auto with bool. + LetTac H3:=(H0 a H2). + Rewrite in_dom_put in H3. + Trivial. +Save. + +Lemma CG_path_last + : (l:(list ad)) (last:ad) (d:D) + (CG_path last d l) -> {l':(list ad) | l=(app l' (cons last (nil ad)))}. + Proof. + Induction 1; Intros. + Exists (nil ad); Simpl; Rewrite e; Trivial. + Case H0; Intros l' H1. + Exists (cons x l'); Simpl. + Rewrite H1; Auto. + Qed. + +(*s The length of a path without repetition is less than the + cardinal of the map representing the graph *) + +Lemma ad_simple_path_bounded_card + : (l:(list ad)) (last,x:ad) (d:D) + (CG_path last d (cons x l)) -> (ad_list_stutters (cons x l))=false + -> (le (length (cons x l)) (S (MapCard ? cg))). + Proof. + Intros. Apply le_trans with m:=(MapCard ? (MapPut ? (MapDom ? cg) last tt)). + Rewrite (ad_list_not_stutters_card (cons x l) H0). Apply MapSubset_Card_le. + Apply CG_path_in_cg_1 with 1:=H; Trivial. + Rewrite (MapCard_Dom ? cg). Apply MapCard_Put_ub. + Qed. + +Lemma CG_path_app_1 : (l1,l2:(list ad)) (last,x:ad) (d1,d2:D) + (CG_path last d2 (cons x l2)) -> (CG_path x d1 l1) -> + (CG_path last (Dplus d2 d1) (app l1 l2)). + Proof. + Intros. + Elim H0; Intros. + Simpl; Rewrite Dplus_d_z; Rewrite e; Trivial. + Rewrite <- Dplus_assoc. + Simpl; Constructor; Auto. + Save. + +Lemma CG_path_app_2 : (l1,l2:(list ad)) (last,x:ad) (d:D) + (CG_path last d (app l1 (cons x l2))) -> + {d2 : D & (CG_path last d2 (cons x l2))}. + Proof. + Induction l1. Simpl. Intros. Split with d. Assumption. + Simpl. Induction l. Intros. Simpl in H0. Inversion H0. Split with d0. Assumption. + Intros. Simpl in H1. Inversion H1. Exact (H0 l2 last x d0 H5). + Qed. + +Lemma CG_path_app_3 : (l1,l2:(list ad)) (last,x:ad) (d:D) + (CG_path last d (app l1 (cons x l2))) -> + {d1 : D & (CG_path x d1 (app l1 (cons x (nil ad))))}. + Proof. + Induction l1. Simpl. Intros. Split with Dz. Apply CG_p1. Reflexivity. + Induction l. Simpl. Intros. Inversion H0. Split with d'. Rewrite <- (Dplus_z_d d'). + Apply CG_p2. Apply CG_p1. Reflexivity. + Assumption. + Simpl. Intros. Inversion H1. Elim (H0 ? ? ? ? H5). Intros d1 H9. Split with (Dplus d1 d'). + Apply CG_p2. Assumption. + Assumption. + Qed. + +Lemma CG_path_weight_and_last_unique + : (l:(list ad)) (last,last':ad) (d,d':D) + (CG_path last d l) -> (CG_path last' d' l) -> d=d' /\ last=last'. + Proof. + Intros l last last' d d' H; Generalize d'. + Elim H; Intros. + Inversion H0. + Split; Trivial. Transitivity x; Auto. + Inversion H1. + Case H0 with 1:=H5; Split; Intros; Trivial. + Rewrite H8. + Replace d'0 with d'2; Auto. + Cut (SOME D d'2)=(SOME D d'0). + Intro E; Injection E; Trivial. + Transitivity (CG_edge x y); Auto. + Qed. + + Inductive and_sp [A:Set; B:Prop] : Set := conj_sp : A -> B -> (and_sp A B). + +(*s Given a path, one may find a shortest path withour repetition *) + +Lemma ad_path_then_simple_path : + (l:(list ad)) (last:ad) (d:D) + (CG_path last d l) -> + {sl:(list ad) & {d0:D & + (and_sp (CG_path last d0 (cons (first l) sl)) + ((ad_list_stutters (cons (first l) sl))=false /\ + (Dle d0 d)=true))}}. + Proof. + Induction 1; Unfold first; Intros. + Exists (nil ad); Exists Dz; Split; Auto. + Constructor; Auto. + Case H0; Clear H0; Intros sl (d1,(H1,(H2,H3))). + Elim (sumbool_of_bool (ad_in_list x (cons y sl))); Intro. + Case (ad_in_list_forms_circuit x (cons y sl) a); Intros. + Case s; Clear a s; Intros l2 H4. + Case (CG_path_app_2 x0 l2 last x d1). + Rewrite <- H4; Trivial. + Intros d2 H5; Exists l2; Exists d2. + Split; Trivial. + Split. + Apply (ad_list_stutters_app_conv_r x0). + Rewrite <- H4; Trivial. + Apply Dle_trans with (Dplus d1 d'). + Case (CG_path_app_3 (cons x x0) l2 last x (Dplus d1 d')). + Simpl; Rewrite <- H4; Constructor; Trivial. + Intros d3 H6. + Replace (Dplus d1 d') with (Dplus d2 d3). + Apply Dle_trans with (Dplus d2 Dz). + Rewrite Dplus_d_z; Auto. + Apply Dle_plus_mono; Trivial. + Apply (no_bad_cycles x d3 (app x0 (cons x (nil ad)))); Auto. + Case (CG_path_weight_and_last_unique + (app (app (cons x x0) (cons x (nil ad))) l2) + last last (Dplus d2 d3) (Dplus d1 d')); Auto. + Apply CG_path_app_1 with x; Trivial. + Replace (app (app (cons x x0) (cons x (nil ad))) l2) + with (cons x (cons y sl)); Auto. + Constructor; Auto. + Rewrite H4; Rewrite <- ass_app; Simpl; Trivial. + Apply Dle_plus_mono; Trivial. + Exists (cons y sl); Exists (Dplus d1 d'); Repeat Split; Auto. + Constructor; Auto. + Change (orb (ad_in_list x (cons y sl)) (ad_list_stutters (cons y sl))) = false. + Apply orb_false_intro; Trivial. + Qed. + +Lemma CG_path_app_4 : (l1,l2:(list ad)) (last,x:ad) (d:D) + (CG_path last d (app l1 (cons x l2))) -> + {d1 : D & {d2 : D & + (and_sp (CG_path x d1 (app l1 (cons x (nil ad)))) * + (CG_path last d2 (cons x l2)) + d=(Dplus d2 d1))}}. + Proof. + Intros. Elim (CG_path_app_2 l1 l2 last x d). Intros d1 H0. + Elim (CG_path_app_3 l1 l2 last x d). Intros d2 H1. Split with d2. Split with d1. + Split. Exact (H1,H0). + Cut (app l1 (cons x l2))=(app (app l1 (cons x (nil ad))) l2). + Intro. Rewrite H2 in H. + Elim (CG_path_weight_and_last_unique ? ? ? ? ? H + (CG_path_app_1 (app l1 (cons x (nil ad))) l2 last x d2 d1 H0 H1)). + Trivial. + Exact (ass_app l1 (cons x (nil ad)) l2). + Assumption. + Assumption. + Qed. + +(*s [(ad_simple_path_naive_search x y prefix n)] is true when + there esists a path [x::l] from [y] to [x] of length less than + [n] with edges not in prefix +*) + +Fixpoint ad_simple_path_naive_search [x,y:ad; l:(list ad); n:nat] : bool := + (orb (ad_eq x y) + Cases n of + O => false + | (S n') => Cases (MapGet ? cg x) of + NONE => false + | (SOME edges) => + let l'=(cons x l) in (* builds reverse path *) + Cases (MapSweep D + [z:ad][d:D] if (ad_in_list z l') + then false + else (ad_simple_path_naive_search z y l' n') + edges) of + NONE => false + | (SOME _) => true + end + end + end). + +Lemma ad_simple_path_naive_search_correct_1 + : (n:nat) (x,y:ad) (l:(list ad)) (d:D) + (le (length l) n) -> (CG_path y d (cons x l)) -> + (prefix:(list ad)) + (ad_list_stutters (app (rev prefix) (cons x l)))=false -> + (ad_simple_path_naive_search x y prefix n)=true. + Proof. + Induction n. Intros x y l. Case l. Intros. Inversion H0. + Rewrite H4. Simpl. + Rewrite (ad_eq_correct y). Reflexivity. + Intros. Elim (le_Sn_O ? H). + Intros n0 H x y l. Case l. Intros. Inversion H1. Rewrite H5. Simpl. + Rewrite (ad_eq_correct y). Reflexivity. + Intros. Simpl. Elim (sumbool_of_bool (ad_eq x y)). Intro H3. Rewrite H3. Reflexivity. + Intro H3. Rewrite H3. Simpl. Elim (option_sum ? (MapGet ? cg x)). Intro H4. Elim H4. + Clear H4. Intros edges H4. Rewrite H4. Inversion_clear H1. Unfold CG_edge in H6. + Rewrite H4 in H6. Elim (option_sum ? (MapGet D edges a)). Intro H7. Elim H7. Clear H7. + Intros d'' H7. Rewrite H7 in H6. + Cut (if (ad_in_list a (cons x prefix)) + then false + else (ad_simple_path_naive_search a y (cons x prefix) n0))=true. + Intro. Elim (MapSweep_semantics_4 D [z:ad] [_:D] + (if (orb (ad_eq z x) (ad_in_list z prefix)) + then false + else (ad_simple_path_naive_search z y (cons x prefix) n0)) + edges a d'' H7 H1). + Intros a' H8. Elim H8. Intros d1 H9. Rewrite H9. Reflexivity. + Rewrite (ad_list_app_rev prefix (cons a l0) x) in H2. + Rewrite <- (ad_in_list_rev (cons x prefix) a). + Rewrite (ad_list_stutters_prev_conv_l ? ? ? H2). + Exact (H a y l0 d0 (le_S_n ? ? H0) H5 (cons x prefix) H2). + Intro H7. Rewrite H7 in H6. Discriminate H6. + Intro H4. Inversion_clear H1. Unfold CG_edge in H6. Rewrite H4 in H6. Discriminate H6. + Qed. + +Lemma ad_simple_path_naive_search_correct + : (n:nat) (x,y:ad) (l:(list ad)) (d:D) + (le (length l) n) -> (CG_path y d (cons x l)) + -> (ad_list_stutters (cons x l))=false + -> (ad_simple_path_naive_search x y (nil ad) n)=true. + Proof. + Intros. Exact (ad_simple_path_naive_search_correct_1 n x y l d H H0 (nil ad) H1). + Qed. + +Lemma ad_simple_path_naive_search_complete_1 + : (n:nat) (x,y:ad) (prefix:(list ad)) + (d':D) (CG_path x d' (rev (cons x prefix))) -> + (ad_list_stutters (cons x prefix))=false -> + (ad_simple_path_naive_search x y prefix n)=true -> + {d:D & {l:(list ad) & (and_sp (CG_path y d (app (rev (cons x prefix)) l)) + (ad_list_stutters (app (rev (cons x prefix)) l)) + =false)}}. + Proof. + Induction n. Intros. Split with d'. Split with (nil ad). Simpl in H1. + Rewrite (orb_b_false (ad_eq x y)) in H1. Rewrite <- (ad_eq_complete ? ? H1). + Rewrite <- app_nil_end. Split. Assumption. + Rewrite ad_list_stutters_rev. Assumption. + Intros. Simpl in H2. Elim (orb_true_elim ? ? H2). Intro H3. + Rewrite <- (ad_eq_complete ? ? H3). Split with d'. Split with (nil ad). + Rewrite <- app_nil_end. Split. Assumption. + Rewrite ad_list_stutters_rev. Assumption. + Intro H3. Clear H2. Elim (option_sum ? (MapGet ? cg x)). Intro H4. Elim H4. + Intros edges H5. Rewrite H5 in H3. + Elim (option_sum ? (MapSweep D [z:ad] [_:D] + (if (orb (ad_eq z x) (ad_in_list z prefix)) + then false + else (ad_simple_path_naive_search z y (cons x prefix) n0)) edges)). + Intro H2. Elim H2. Intro r. Elim r. Intros x0 d0 H6. + Cut (if (ad_in_list x0 (cons x prefix)) + then false + else (ad_simple_path_naive_search x0 y (cons x prefix) n0))=true. + Intro. Elim (sumbool_of_bool (ad_in_list x0 (cons x prefix))). Intro H8. + Rewrite H8 in H7. Discriminate H7. + Intro H8. Rewrite H8 in H7. Clear H2 H3. Elim (H x0 y (cons x prefix) (Dplus d0 d')). + Intros d1 H9. Elim H9. Intros l H10. Elim H10. Intros H11 H12. + Rewrite <- (ad_list_app_rev (cons x prefix) l x0) in H11. + Rewrite <- (ad_list_app_rev (cons x prefix) l x0) in H12. Split with d1. + Split with (cons x0 l). Split. Assumption. + Assumption. + Change (CG_path x0 (Dplus d0 d') (app (rev (cons x prefix)) (cons x0 (nil ad)))). + Apply CG_path_app_1 with x:=x. Rewrite <- (Dplus_z_d d0). Apply CG_p2. Apply CG_p1. + Reflexivity. + Unfold CG_edge. Rewrite H5. Rewrite (MapSweep_semantics_2 ? ? edges x0 d0 H6). + Reflexivity. + Assumption. + Simpl. Simpl in H1. Rewrite H1. Simpl in H8. Rewrite H8. Reflexivity. + Assumption. + Exact (MapSweep_semantics_1 ? ? ? x0 d0 H6). + Intro H2. Rewrite H2 in H3. Discriminate H3. + Intro H4. Rewrite H4 in H3. Discriminate H3. + Qed. + +Lemma ad_simple_path_naive_search_complete : (n:nat) (x,y:ad) + (ad_simple_path_naive_search x y (nil ad) n)=true -> + {d:D & {l:(list ad) & (and_sp (CG_path y d (cons x l)) + (ad_list_stutters (cons x l))=false)}}. + Proof. + Intros. Exact (ad_simple_path_naive_search_complete_1 n x y (nil ad) Dz + (CG_p1 x x (refl_equal ? ?)) (refl_equal ? false) H). + Qed. + +(*s Definition of simple paths : paths without repetition *) + +Definition CG_simple_path := [last:ad] [d:D] [l:(list ad)] + (and_sp (CG_path last d l) (ad_list_stutters l)=false). + +(*s Between two vertexes, there exists a simple path or there exists no path *) +Lemma ad_simple_path_dec : (x,y:ad) + {l:(list ad) & {d:D & (CG_simple_path y d (cons x l))}}+ + {(l:(list ad)) (d:D) (CG_simple_path y d (cons x l)) -> False}. + Proof. + Intros. Elim (sumbool_of_bool (ad_simple_path_naive_search x y (nil ad) (MapCard ? cg))). + Intro H. Left . Elim (ad_simple_path_naive_search_complete ? ? ? H). Intros d H0. + Elim H0. Intros l H1. Split with l. Split with d. Exact H1. + Intro H. Right . Intros l d H0. Unfold CG_simple_path in H0. Elim H0. Intros H1 H2. + Rewrite (ad_simple_path_naive_search_correct ? x y l d + (le_S_n ? ? (ad_simple_path_bounded_card ? ? ? ? H1 H2)) H1 H2) in H. + Discriminate H. + Qed. + +(*s Computing the minimum of edges in a Map *) + +Definition all_min := [f:ad->D->(option D)] (MapFold ? ? (NONE D) Ddmin f). + +Lemma all_min_le_1 : (f:ad->D->(option D)) (m:(Map D)) + (a:ad) (d:D) (MapGet ? m a)=(SOME ? d) -> + (Ddle (all_min f m) (f a d))=true. + Proof. + Intros. Elim (option_sum ? (f a d)). Intro H0. Elim H0. Intros d' H1. Rewrite H1. + Unfold all_min. Cut ([a:(option D)][b:D](Ddle a (SOME D b)) + (MapFold D (option D) (NONE D) Ddmin f m) d') + =(MapFold D bool false orb + [a:ad] [y:D]([a0:(option D)][b:D](Ddle a0 (SOME D b)) (f a y) d') m). + Intro. Rewrite H2. Rewrite MapFold_orb. + Elim (MapSweep_semantics_4 D [a:ad][y:D](Ddle (f a y) (SOME D d')) m a d H). + Intros a' H3. Elim H3. Intros d'' H4. Rewrite H4. Reflexivity. + Rewrite H1. Simpl. Apply Dle_refl. + Exact (MapFold_distr_r D ? (NONE D) Ddmin bool false orb D + [a:(option D)][b:D](Ddle a (SOME D b)) + [c:D](refl_equal ? false) + [a,b:(option D)][c:D](Ddmin_le_distr_l a b (SOME ? c)) f m d'). + Intro H0. Rewrite H0. (Case (all_min f m); Reflexivity). + Qed. + +Lemma all_min_le_2_1 : (f:ad->D->(option D)) (m:(Map D)) (pf:ad->ad) + (d:D) (MapFold1 ? ? (NONE D) Ddmin f pf m)=(SOME ? d) -> + {a:ad & {d':D | (MapGet ? m a)=(SOME ? d') /\ (f (pf a) d')=(SOME ? d)}}. + Proof. + Induction m. Intros. Discriminate H. + Intros a y pf d H. Simpl in H. Split with a. Split with y. Split. Apply M1_semantics_1. + Assumption. + Intros. Simpl in H1. + Elim (Ddmin_choice + (MapFold1 D (option D) (NONE D) Ddmin f [a0:ad](pf (ad_double a0)) m0) + (MapFold1 D (option D) (NONE D) Ddmin f [a0:ad](pf (ad_double_plus_un a0)) m1)). + Intro H2. Rewrite H2 in H1. Elim (H [a0:ad](pf (ad_double a0)) d H1). Intros a0 H3. + Elim H3. Intros d' H4. Split with (ad_double a0). Split with d'. Split. + Rewrite MapGet_M2_bit_0_0. Rewrite ad_double_div_2. (Elim H4; Trivial). + Apply ad_double_bit_0. + (Elim H4; Trivial). + Intro H2. Rewrite H2 in H1. Elim (H0 [a0:ad](pf (ad_double_plus_un a0)) d H1). + Intros a0 H3. Elim H3. Intros d' H4. Split with (ad_double_plus_un a0). Split with d'. + Split. Rewrite MapGet_M2_bit_0_1. Rewrite ad_double_plus_un_div_2. (Elim H4; Trivial). + Apply ad_double_plus_un_bit_0. + (Elim H4; Trivial). + Qed. + +Lemma all_min_le_2 : (f:ad->D->(option D)) (m:(Map D)) + (d:D) (all_min f m)=(SOME ? d) -> + {a:ad & {d':D | (MapGet ? m a)=(SOME ? d') /\ (f a d')=(SOME ? d)}}. + Proof. + Intros. Exact (all_min_le_2_1 f m [a:ad]a d H). + Qed. + +Lemma all_min_le_3 : (f,g:ad->D->(option D)) (m:(Map D)) + ((a:ad) (d:D) (MapGet ? m a)=(SOME ? d) -> (Ddle (f a d) (g a d))=true) -> + (Ddle (all_min f m) (all_min g m))=true. + Proof. + Intros. Elim (option_sum ? (all_min g m)). Intro H0. Elim H0. Intros d H1. + Elim (all_min_le_2 g m d H1). Intros a H2. Elim H2. Intros d' H3. Elim H3. Intros H4 H5. + Apply Ddle_trans with (f a d'). Apply all_min_le_1. Assumption. + Rewrite H1. Rewrite <- H5. Apply H. Assumption. + Intro H0. Rewrite H0. Apply Ddle_d_none. + Qed. + +(*s [(ad_simple_path_dist_1 x y l n)] computes the minimum weight of a path + from [x] to [y] of maximal length [n] which does not contain vertexes + from [l] *) + +Fixpoint ad_simple_path_dist_1 [x,y:ad; l:(list ad); n:nat] : (option D) := + if (ad_eq x y) + then (SOME ? Dz) + else + Cases n of + O => (NONE ?) + | (S n') => Cases (MapGet ? cg x) of + NONE => (NONE ?) + | (SOME edges) => + let l'=(cons x l) in (* builds reverse path *) + (all_min [z:ad][d:D] + if (ad_in_list z l') + then (NONE D) + else (Ddplus (ad_simple_path_dist_1 z y l' n') d) + edges) + end + end. + +Lemma ad_simple_path_dist_1_correct_1 : (n:nat) (x,y:ad) (l:(list ad)) (d:D) + (le (length l) n) -> (CG_path y d (cons x l)) -> + (prefix:(list ad)) + (ad_list_stutters (app (rev prefix) (cons x l)))=false -> + (Ddle (ad_simple_path_dist_1 x y prefix n) (SOME ? d))=true. + Proof. + Induction n. Intros x y l. Case l. Intros. Inversion H0. + Rewrite H4. Simpl. + Rewrite (ad_eq_correct y). Rewrite H3. Apply Ddle_refl. + Intros. Elim (le_Sn_O ? H). + Intros n0 H x y l. Case l. Intros. Inversion H1. + Rewrite H5. Simpl. + Rewrite (ad_eq_correct y). Rewrite H4. Apply Ddle_refl. + Intros. Simpl. Elim (sumbool_of_bool (ad_eq x y)). Intro H3. Rewrite H3. + Rewrite (ad_eq_complete ? ? H3) in H1. Exact (no_bad_cycles ? ? ? H1). + Intro H3. Rewrite H3. Elim (option_sum ? (MapGet ? cg x)). Intro H4. Elim H4. + Intros edges H5. Rewrite H5. Inversion_clear H1. + Apply Ddle_trans with dd':=Case (ad_in_list a (cons x prefix)) of + (NONE D) + (Ddplus (ad_simple_path_dist_1 a y (cons x prefix) n0) d') + end. + Cut (MapGet ? edges a)=(SOME ? d'). Intro. + Exact (all_min_le_1 [z:ad] [d:D] + Case (orb (ad_eq z x) (ad_in_list z prefix)) of + (NONE D) + (Ddplus (ad_simple_path_dist_1 z y (cons x prefix) n0) d) + end edges a d' H1). + Unfold CG_edge in H7. Rewrite H5 in H7. Elim (option_sum ? (MapGet D edges a)). Intro H8. + Elim H8. Intros d1 H9. Rewrite H9 in H7. Rewrite H9. Inversion_clear H7. Reflexivity. + Intro H8. Rewrite H8 in H7. Discriminate H7. + Rewrite (ad_list_app_rev prefix (cons a l0) x) in H2. + Rewrite <- (ad_in_list_rev (cons x prefix) a). + Rewrite (ad_list_stutters_prev_conv_l ? ? ? H2). + Apply (Ddle_plus_mono (ad_simple_path_dist_1 a y (cons x prefix) n0) (SOME D d0) d' d'). + Exact (H a y l0 d0 (le_S_n ? ? H0) H6 (cons x prefix) H2). + Apply Dle_refl. + Intro H4. Inversion H1. Unfold CG_edge in H10. + Rewrite H4 in H10. Discriminate H10. + Qed. + +Lemma ad_simple_path_dist_1_correct_2 : (n:nat) (x,y:ad) (l:(list ad)) (d:D) + (le (length l) n) -> (CG_path y d (cons x l)) -> + (ad_list_stutters (cons x l))=false -> + (Ddle (ad_simple_path_dist_1 x y (nil ad) n) (SOME ? d))=true. + Proof. + Intros. Exact (ad_simple_path_dist_1_correct_1 n x y l d H H0 (nil ad) H1). + Qed. + +(*s [(ad_simple_path_dist x y)] computes the minimum path from x to y *) +Definition ad_simple_path_dist := [x,y:ad] + (ad_simple_path_dist_1 x y (nil ad) (MapCard ? cg)). + +Lemma ad_simple_path_dist_correct_1 : (x,y:ad) (l:(list ad)) (d:D) + (CG_path y d (cons x l)) -> + (ad_list_stutters (cons x l))=false -> + (Ddle (ad_simple_path_dist x y) (SOME ? d))=true. + Proof. + Intros. Unfold ad_simple_path_dist. + (Apply ad_simple_path_dist_1_correct_2 with l:=l; Try Assumption). + Exact (le_S_n ? ? (ad_simple_path_bounded_card l y x d H H0)). + Qed. + +Lemma ad_simple_path_dist_correct : (x,y:ad) (l:(list ad)) (d:D) + (CG_path y d (cons x l)) -> + (Ddle (ad_simple_path_dist x y) (SOME ? d))=true. + Proof. + Intros. Elim ad_path_then_simple_path with 1:= H. + Intros l0 H0. + Elim H0. Intros d0 H1. Elim H1. Intros H2 H3. Elim H3. Intros H4 H5. + Apply Ddle_trans with dd':=(SOME D d0). + Exact (ad_simple_path_dist_correct_1 x y l0 d0 H2 H4). + Exact H5. + Qed. + +Lemma ad_simple_path_dist_1_complete_1 : (n:nat) (x,y:ad) (prefix:(list ad)) + (d':D) (CG_path x d' (rev (cons x prefix))) -> + (ad_list_stutters (cons x prefix))=false -> + (d0:D) + (ad_simple_path_dist_1 x y prefix n)=(SOME D d0) -> + {l:(list ad) & (and_sp (CG_path y (Dplus d0 d') (app (rev (cons x prefix)) l)) + (ad_list_stutters (app (rev (cons x prefix)) l))=false /\ + (le (length l) n) )}. + Proof. + Induction n. Intros. Split with (nil ad). Split. Unfold ad_simple_path_dist_1 in H1. + Elim (sumbool_of_bool (ad_eq x y)). Intro H2. Rewrite H2 in H1. Inversion H1. + Rewrite <- H4. Rewrite Dplus_z_d. Rewrite <- app_nil_end. + Rewrite <- (ad_eq_complete ? ? H2). Assumption. + Intro H2. Rewrite H2 in H1. Discriminate H1. + Split. Rewrite <- app_nil_end. Rewrite ad_list_stutters_rev. Assumption. + Apply le_n. + Intros. Simpl in H2. Elim (sumbool_of_bool (ad_eq x y)). Intro H3. Rewrite H3 in H2. + Inversion H2. Split with (nil ad). Split. Rewrite <- H5. Rewrite Dplus_z_d. + Rewrite <- app_nil_end. Rewrite <- (ad_eq_complete ? ? H3). Assumption. + Split. Rewrite <- app_nil_end. Rewrite ad_list_stutters_rev. Assumption. + Apply le_O_n. + Intro H3. Rewrite H3 in H2. Elim (option_sum ? (MapGet ? cg x)). Intro H4. Elim H4. + Intros edges H5. Rewrite H5 in H2. Elim (all_min_le_2 ? edges d0 H2). Intros a H6. + Elim H6. Intros d1 H7. Elim H7. Intros H8 H9. Clear H2 H6 H7. + Cut (ad_in_list a (cons x prefix))=false. Intro. + Elim (option_sum ? (ad_simple_path_dist_1 a y (cons x prefix) n0)). Intro H6. Elim H6. + Intros d2 H7. Clear H6. Rewrite H7 in H9. Cut (Dplus d2 d1)=d0. Intro. + Cut (CG_path a (Dplus d1 d') (rev (cons a (cons x prefix)))). Intro. + Cut (ad_list_stutters (cons a (cons x prefix)))=false. Intro. + Elim (H a y (cons x prefix) ? H10 H11 d2 H7). Intros l0 H12. Elim H12. Intros H13 H14. + Elim H14. Intros H15 H16. Split with (cons a l0). Split. Rewrite ad_list_app_rev. + Rewrite <- H6. Rewrite Dplus_assoc. Assumption. + Split. Rewrite ad_list_app_rev. Assumption. + Exact (le_n_S ? ? H16). + Simpl. Simpl in H2. Rewrite H2. Simpl in H1. Rewrite H1. Reflexivity. + Apply (CG_path_app_1 (rev (cons x prefix)) (cons a (nil ad)) a x). + Rewrite <- (Dplus_z_d d1). Apply CG_p2. Apply CG_p1. Reflexivity. + Unfold CG_edge. Rewrite H5. Rewrite H8. Reflexivity. + Assumption. + Elim (sumbool_of_bool (orb (ad_eq a x) (ad_in_list a prefix))). Intro H10. + Rewrite H10 in H9. Discriminate H9. + Intro H10. Rewrite H10 in H9. Simpl in H9. Inversion H9. Reflexivity. + Intro H6. Rewrite H6 in H9. Generalize H9. + Case (orb (ad_eq a x) (ad_in_list a prefix)); Intro H10; Discriminate H10. + Elim (sumbool_of_bool (ad_in_list a (cons x prefix))). Intro H10. Simpl in H10. + Rewrite H10 in H9. Discriminate H9. + Trivial. + Intro H4. Rewrite H4 in H2. Discriminate H2. + Qed. + +Lemma ad_simple_path_dist_1_complete : (n:nat) (x,y:ad) (d:D) + (ad_simple_path_dist_1 x y (nil ad) n)=(SOME D d) -> + {l:(list ad) & (and_sp (CG_path y d (cons x l)) + (ad_list_stutters (cons x l))=false)}. + Proof. + Intros. Elim (ad_simple_path_dist_1_complete_1 n x y (nil ad) Dz + (CG_p1 x x (refl_equal ? ?)) (refl_equal ? ?) d H). + Intros l H0. Split with l. Elim H0. Intros H1 H2. Elim H2. Intros H3 H4. Split. + Rewrite (Dplus_d_z d) in H1. Assumption. + Exact H3. + Qed. + +Lemma ad_simple_path_dist_complete : (x,y:ad) (d:D) + (ad_simple_path_dist x y)=(SOME D d) -> + {l:(list ad) & (and_sp (CG_path y d (cons x l)) + (ad_list_stutters (cons x l))=false)}. + Proof. + Intros. Exact (ad_simple_path_dist_1_complete (MapCard ? cg) x y d H). + Qed. + +Lemma ad_simple_path_dist_complete_2 : (x,y:ad) (d:D) + (ad_simple_path_dist x y)=(SOME D d) -> + {l:(list ad) & (CG_path y d (cons x l))}. + Proof. + Intros. Elim (ad_simple_path_dist_complete x y d H). Intros l H0. Split with l. + (Elim H0; Trivial). + Qed. + +Lemma ad_simple_path_dist_complete_3 : (x,y:ad) (dd:(option D)) + ((l:(list ad)) (d:D) (CG_path y d (cons x l)) -> (Ddle dd (SOME ? d))=true) -> + (Ddle dd (ad_simple_path_dist x y))=true. + Proof. + Intros x y dd. Case dd. Intros. Elim (option_sum ? (ad_simple_path_dist x y)). Intro H0. + Elim H0. Intros d H1. Elim (ad_simple_path_dist_complete_2 x y d H1). Intros l H2. + Simpl in H. Rewrite <- (H l d H2). Rewrite H1. Reflexivity. + Intro H0. Rewrite H0. Reflexivity. + Intros. Elim (option_sum ? (ad_simple_path_dist x y)). Intro H0. Elim H0. Intros d0 H1. + Rewrite H1. Elim (ad_simple_path_dist_complete_2 x y d0 H1). Intros l H2. + Exact (H l d0 H2). + Intro H0. Rewrite H0. Reflexivity. + Qed. + +Lemma ad_simple_path_dist_d_1 : (x:ad) (ad_simple_path_dist x x)=(SOME ? Dz). + Proof. + Unfold ad_simple_path_dist. (Elim (MapCard ? cg); Simpl). Intro. + Rewrite (ad_eq_correct x). Reflexivity. + Intros. Rewrite (ad_eq_correct x). Reflexivity. + Qed. + +Lemma ad_simple_path_dist_d_2 : (x,y,z:ad) (d,d':D) + (ad_simple_path_dist x y)=(SOME ? d) -> (ad_simple_path_dist y z)=(SOME ? d') -> + (Ddle (ad_simple_path_dist x z) (SOME ? (Dplus d' d)))=true. + Proof. + Intros. Elim (ad_simple_path_dist_complete_2 x y d H). + Elim (ad_simple_path_dist_complete_2 y z d' H0). Intros l1 H1 l2 H2. + Apply (ad_simple_path_dist_correct x z (app l2 l1)). + Exact (CG_path_app_1 (cons x l2) l1 z y d d' H1 H2). + Qed. + +Lemma ad_simple_path_dist_d_3 : (x,y,z:ad) (d,d':D) + (Ddle (ad_simple_path_dist x y) (SOME ? d))=true -> + (Ddle (ad_simple_path_dist y z) (SOME ? d'))=true -> + (Ddle (ad_simple_path_dist x z) (SOME ? (Dplus d' d)))=true. + Proof. + Intros. Elim (option_sum ? (ad_simple_path_dist x y)). Intro H1. Elim H1. Intros d0 H2. + Elim (option_sum ? (ad_simple_path_dist y z)). Intro H3. Elim H3. Intros d'0 H4. + Apply Ddle_trans with dd':=(SOME D (Dplus d'0 d0)). + Exact (ad_simple_path_dist_d_2 x y z d0 d'0 H2 H4). + Rewrite H2 in H. Simpl in H. Rewrite H4 in H0. Simpl in H0. Simpl. + Exact (Dle_plus_mono ? ? ? ? H0 H). + Intro H3. Rewrite H3 in H0. Discriminate H0. + Intro H1. Rewrite H1 in H. Discriminate H. + Qed. + +(*s [(CG_leq x y)] is true when there is a path from [x] to [y] *) + +Definition CG_leq := [x,y:ad] Cases (ad_simple_path_dist x y) of + (SOME _) => true + | _ => false + end. + +Lemma CG_leq_refl : (x:ad) (CG_leq x x)=true. + Proof. + Unfold CG_leq. Intros. Rewrite (ad_simple_path_dist_d_1 x). Reflexivity. + Qed. + +Lemma CG_leq_trans : (x,y,z:ad) (CG_leq x y)=true -> (CG_leq y z)=true -> (CG_leq x z)=true. + Proof. + Unfold CG_leq. Intros. Elim (option_sum ? (ad_simple_path_dist x y)). Intro H1. + Elim H1. Intros d1 H2. Elim (option_sum ? (ad_simple_path_dist y z)). Intro H3. + Elim H3. Intros d2 H4. Cut (Ddle (ad_simple_path_dist x z) (SOME D (Dplus d2 d1)))=true. + Intro. Elim (option_sum ? (ad_simple_path_dist x z)). Intro H6. Elim H6. Intros d3 H7. + Rewrite H7. Reflexivity. + Intro H6. Rewrite H6 in H5. Discriminate H5. + Exact (ad_simple_path_dist_d_2 ? ? ? ? ? H2 H4). + Intro H3. Rewrite H3 in H0. Discriminate H0. + Intro H1. Rewrite H1 in H. Discriminate H. + Qed. + +(*s [(CG_standard_rho root d0 others x)] computes [d0-d] when + [root] and [x] are connected by a path of minimal + length [d] and [(others x)] when there are not connected +*) + +Definition CG_standard_rho + := [root:ad] [d0:D] [others:ad->D] [x:ad] + Cases (ad_simple_path_dist root x) of + (SOME d) => (Dplus d0 (Dneg d)) + | NONE => (others x) (* dummy *) + end. + +Lemma CG_standard_rho_root : (root:ad) (d0:D) (others:ad->D) + (CG_standard_rho root d0 others root)=d0. + Proof. + Unfold CG_standard_rho. Intros. Rewrite (ad_simple_path_dist_d_1 root). + Rewrite Dneg_Dz. Apply Dplus_d_z. + Qed. + +(*s If there is a root such that all the nodes ae connected to + this root, then [CG_standard_rho] gives a correct valuation +*) +Lemma CG_rooted_sat_1 : (root:ad) (d0:D) (others:ad->D) + ((x:ad) (in_dom ? x cg)=true -> (CG_leq root x)=true) -> + (CGsat (CG_standard_rho root d0 others)). + Proof. + Unfold CG_standard_rho. Intros. Unfold CGsat. Intros. + Elim (option_sum ? (ad_simple_path_dist root x)). Intro H1. Elim H1. Intros d1 H2. + Rewrite H2. Cut (Ddle (ad_simple_path_dist root y) (SOME D (Dplus d d1)))=true. Intro. + Elim (option_sum ? (ad_simple_path_dist root y)). Intro H4. Elim H4. Intros d2 H5. + Rewrite H5. Rewrite Dplus_assoc. Apply Dle_plus_mono. Apply Dle_refl. + Apply Dplus_reg_l with d'':=d2. Rewrite <- Dplus_assoc. Rewrite Dplus_neg. + Rewrite Dplus_z_d. Apply Dplus_reg_r with d'':=d1. Rewrite Dplus_assoc. + Rewrite Dplus_neg_2. Rewrite Dplus_d_z. Rewrite H5 in H3. Exact H3. + Intro H4. Rewrite H4 in H3. Discriminate H3. + Elim (ad_simple_path_dist_complete_2 root x d1 H2). Intros l H3. + Apply (ad_simple_path_dist_correct root y (app l (cons y (nil ad))) (Dplus d d1)). + Change (CG_path y (Dplus d d1) (app (cons root l) (cons y (nil ad)))). + Apply CG_path_app_1 with last:=y x:=x. Rewrite <- (Dplus_z_d d). Apply CG_p2. + Apply CG_p1. Reflexivity. + Assumption. + Assumption. + Intro H1. Cut (CG_leq root x)=true. + Unfold CG_leq. Rewrite H1. Intro. Discriminate H2. + Apply H. Rewrite MapDom_Dom. Exact (CG_edge_in_cg_1 ? ? ? H0). + Qed. + +Lemma CG_rooted_sat : (root:ad) (d0:D) + ((x:ad) (in_dom ? x cg)=true -> (CG_leq root x)=true) -> + {rho:ad->D | (CGsat rho) /\ (rho root)=d0}. + Proof. + Intros. Split with (CG_standard_rho root d0 [x:ad]d0). Split. + Exact (CG_rooted_sat_1 root d0 [x:ad]d0 H). + Apply CG_standard_rho_root. + Qed. + +(*s The [CG_standard_rho] valuation is the minimal one *) +Lemma CG_standard_rho_minimal : (root:ad) (d0:D) (others:ad->D) + (rho:ad->D) (CGsat rho) -> (Dle d0 (rho root))=true -> + (x:ad) (CG_leq root x)=true -> + (Dle (CG_standard_rho root d0 others x) (rho x))=true. + Proof. + Unfold CG_leq CG_standard_rho. Intros. Elim (option_sum ? (ad_simple_path_dist root x)). + Intro H2. Elim H2. Intros d H3. Rewrite H3. + Elim (ad_simple_path_dist_complete_2 root x d H3). Intros l H4. + Apply Dplus_reg_r with d'':=d. Rewrite Dplus_assoc. Rewrite Dplus_neg_2. + Rewrite Dplus_d_z. Apply Dle_trans with d':=(rho root). Exact H0. + Exact (CG_path_correct l root x d H4 rho H). + Intro H2. Rewrite H2 in H1. Discriminate H1. + Qed. + +Lemma CG_sat_add_1 : (x,y:ad) (d:D) + (rho:ad->D) (CGsat rho) -> (Dle (rho x) (Dplus (rho y) d))=true -> + (Ddle (SOME ? (Dneg d)) (ad_simple_path_dist y x))=true. + Proof. + Intros. Apply ad_simple_path_dist_complete_3. Intros. Simpl. + Apply Dplus_reg_r with d'':=d. Rewrite Dplus_neg_2. Apply Dplus_reg_l with d'':=(rho x). + Rewrite Dplus_d_z. Apply Dle_trans with d':=(Dplus (rho y) d); Try Assumption. + Apply Dle_trans with d':=(Dplus (Dplus (rho x) d0) d). Apply Dle_plus_mono. + Exact (CG_path_correct l y x d0 H1 rho H). + Apply Dle_refl. + Rewrite Dplus_assoc. Apply Dle_refl. + Qed. + + End CGNoBadCycles. + +(*s [(CG_add x y d)] adds the edge (x,y) of weight d to G, + in case an edge already exists, only the minimal one is kept +*) + +Definition CG_add := [x,y:ad; d:D] + Cases (MapGet ? cg x) of + NONE => (MapPut ? cg x (M1 ? y d)) + | (SOME edges) => Cases (MapGet ? edges y) of + NONE => (MapPut ? cg x (MapPut ? edges y d)) + | (SOME d0) => (MapPut ? cg x (MapPut ? edges y (Dmin d d0))) + end + end. + +End CGDist. + +(*s Properties of [CG_add] *) +Section CGAdd. + + Variable cg1 : CGraph1. + + Variable x,y : ad. + Variable d:D. + +Definition cg2 := (CG_add cg1 x y d). + +Lemma CG_add_edge_1 : (x0,y0:ad) (CG_edge cg2 x0 y0)= + (if (andb (ad_eq x x0) (ad_eq y y0)) + then (Ddmin (SOME ? d) (CG_edge cg1 x0 y0)) + else (CG_edge cg1 x0 y0)). + Proof. + Unfold cg2 CG_add. Intros. Elim (sumbool_of_bool (andb (ad_eq x x0) (ad_eq y y0))). + Intro H. Elim (andb_prop ? ? H). Intros H0 H1. Rewrite H. + Rewrite <- (ad_eq_complete ? ? H0). Rewrite <- (ad_eq_complete ? ? H1). + Elim (option_sum ? (MapGet ? cg1 x)). Intro H2. Elim H2. Intros edges H3. Rewrite H3. + Elim (option_sum ? (MapGet D edges y)). Intro H4. Elim H4. Intros d0 H5. Rewrite H5. + Unfold CG_edge. Rewrite (MapPut_semantics ? cg1 x (MapPut D edges y (Dmin d d0)) x). + Rewrite (ad_eq_correct x). Rewrite (MapPut_semantics ? edges y (Dmin d d0) y). + Rewrite (ad_eq_correct y). Rewrite H3. Rewrite H5. Reflexivity. + Intro H4. Rewrite H4. Unfold CG_edge. + Rewrite (MapPut_semantics ? cg1 x (MapPut D edges y d) x). Rewrite (ad_eq_correct x). + Rewrite H3. Rewrite H4. Rewrite (MapPut_semantics ? edges y d y). + Rewrite (ad_eq_correct y). Reflexivity. + Intro H2. Rewrite H2. Unfold CG_edge. Rewrite (MapPut_semantics ? cg1 x (M1 D y d) x). + Rewrite (ad_eq_correct x). Rewrite H2. Rewrite (M1_semantics_1 ? y d). Reflexivity. + Intro H. Rewrite H. Elim (andb_false_elim ? ? H). Intro H0. + Elim (option_sum ? (MapGet ? cg1 x)). Intro H1. Elim H1. Intros edges H2. Rewrite H2. + Elim (option_sum ? (MapGet ? edges y)). Intro H3. Elim H3. Intros d0 H4. Rewrite H4. + Unfold CG_edge. Rewrite (MapPut_semantics ? cg1 x (MapPut D edges y (Dmin d d0)) x0). + Rewrite H0. Reflexivity. + Intro H3. Rewrite H3. Unfold CG_edge. + Rewrite (MapPut_semantics ? cg1 x (MapPut D edges y d) x0). Rewrite H0. Reflexivity. + Intro H1. Rewrite H1. Unfold CG_edge. Rewrite (MapPut_semantics ? cg1 x (M1 D y d) x0). + Rewrite H0. Reflexivity. + Intro H0. Elim (option_sum ? (MapGet ? cg1 x)). Intro H1. Elim H1. Intros edges H2. + Rewrite H2. Elim (option_sum ? (MapGet ? edges y)). Intro H3. Elim H3. Intros d0 H4. + Rewrite H4. Unfold CG_edge. + Rewrite (MapPut_semantics ? cg1 x (MapPut D edges y (Dmin d d0)) x0). + Elim (sumbool_of_bool (ad_eq x x0)). Intro H5. Rewrite H5. + Rewrite (MapPut_semantics ? edges y (Dmin d d0) y0). Rewrite H0. + Rewrite <- (ad_eq_complete ? ? H5). Rewrite H2. Reflexivity. + Intro H5. Rewrite H5. Reflexivity. + Intro H3. Rewrite H3. Unfold CG_edge. + Rewrite (MapPut_semantics ? cg1 x (MapPut D edges y d) x0). + Elim (sumbool_of_bool (ad_eq x x0)). Intro H4. Rewrite H4. + Rewrite <- (ad_eq_complete ? ? H4). Rewrite H2. + Rewrite (MapPut_semantics ? edges y d y0). Rewrite H0. Reflexivity. + Intro H4. Rewrite H4. Reflexivity. + Intro H1. Rewrite H1. Unfold CG_edge. Rewrite (MapPut_semantics ? cg1 x (M1 D y d) x0). + Elim (sumbool_of_bool (ad_eq x x0)). Intro H2. Rewrite H2. + Rewrite (M1_semantics_2 ? y y0 d H0). Rewrite <- (ad_eq_complete ? ? H2). + Rewrite H1. Reflexivity. + Intro H2. Rewrite H2. Reflexivity. + Qed. + +Lemma CG_add_edge_2 : (x0,y0:ad) (Ddle (CG_edge cg2 x0 y0) (CG_edge cg1 x0 y0))=true. + Proof. + Intros. Rewrite (CG_add_edge_1 x0 y0). + Elim (sumbool_of_bool (andb (ad_eq x x0) (ad_eq y y0))). Intro H. Rewrite H. + Apply Ddmin_le_2. + Intro H. Rewrite H. Apply Ddle_refl. + Qed. + +Lemma CG_add_1 : (rho:ad->D) + (CGsat cg1 rho) -> (Dle (rho x) (Dplus (rho y) d))=true + -> (CGsat cg2 rho). + Proof. + Unfold CGsat. Intros. Rewrite (CG_add_edge_1 x0 y0) in H1. + Elim (sumbool_of_bool (andb (ad_eq x x0) (ad_eq y y0))). Intro H2. + Elim (andb_prop ? ? H2). Intros H3 H4. Rewrite H2 in H1. + Rewrite <- (ad_eq_complete ? ? H3). Rewrite <- (ad_eq_complete ? ? H4). + Elim (option_sum ? (CG_edge cg1 x0 y0)). Intro H5. Elim H5. Intros d1 H6. + Rewrite H6 in H1. Simpl in H1. Inversion H1. Rewrite Dmin_plus_r. Apply Dmin_le_5. + Assumption. + Apply H. Rewrite (ad_eq_complete ? ? H3). Rewrite (ad_eq_complete ? ? H4). Assumption. + Intro H5. Rewrite H5 in H1. Simpl in H1. Inversion H1. Rewrite <- H7. Assumption. + Intro H2. Rewrite H2 in H1. Apply H. Assumption. + Qed. + +Lemma CG_add_2 : (rho:ad->D) (CGsat cg2 rho) -> (CGsat cg1 rho). + Proof. + Unfold CGsat. Intros. Elim (option_sum ? (CG_edge cg2 x0 y0)). Intro H1. Elim H1. + Intros d1 H2. Cut (Dle d1 d0)=true. Intro H3. + Apply Dle_trans with d':=(Dplus (rho y0) d1). Apply H. Assumption. + Apply Dle_plus_mono. Apply Dle_refl. + Assumption. + Change (Ddle (SOME ? d1) (SOME ? d0))=true. Rewrite <- H2. Rewrite <- H0. + Apply CG_add_edge_2. + Intro H1. Cut (Ddle (NONE ?) (SOME ? d0))=true. Intro H2. Discriminate H2. + Rewrite <- H1. Rewrite <- H0. Apply CG_add_edge_2. + Qed. + +Lemma CG_add_3 : (rho:ad->D) (CGsat cg2 rho) -> (Dle (rho x) (Dplus (rho y) d))=true. + Proof. + Unfold CGsat. Intros. Elim (option_sum ? (CG_edge cg2 x y)). Intro H0. Elim H0. + Intros d0 H1. Apply Dle_trans with d':=(Dplus (rho y) d0). Apply H. Assumption. + Apply Dle_plus_mono. Apply Dle_refl. + Rewrite (CG_add_edge_1 x y) in H1. Rewrite (ad_eq_correct x) in H1. + Rewrite (ad_eq_correct y) in H1. Simpl in H1. Elim (option_sum ? (CG_edge cg1 x y)). + Intro H2. Elim H2. Intros d1 H3. Rewrite H3 in H1. Inversion H1. Apply Dmin_le_1. + Intro H2. Rewrite H2 in H1. Inversion H1. Apply Dle_refl. + Intro H0. Rewrite (CG_add_edge_1 x y) in H0. Rewrite (ad_eq_correct x) in H0. + Rewrite (ad_eq_correct y) in H0. Simpl in H0. Generalize H0. + (Case (CG_edge cg1 x y); Intro H1). Discriminate H1. + Intro H2. Discriminate H2. + Qed. + +(*s Every path in the new graph [cg2] either goes through the new edge from [x] to [y], + or is a path in the old graph cg1: +*) +Lemma CG_add_4_1 : (l:(list ad)) (x0,y0:ad) (d0:D) (CG_path cg2 y0 d0 (cons x0 l)) -> + {l0:(list ad) & {l1:(list ad) | (cons x0 l)=(app l0 (cons x (cons y l1)))}}+ + (CG_path cg1 y0 d0 (cons x0 l)). + Proof. + Induction l. Intros. Inversion H. Right . Rewrite H2. + Rewrite <- H1. Apply CG_p1. + Reflexivity. + Intros. Inversion H0. Rewrite (CG_add_edge_1 x0 a) in H6. + Elim (sumbool_of_bool (andb (ad_eq x x0) (ad_eq y a))). Intro H8. Left . + Split with (nil ad). Split with l0. Elim (andb_prop ? ? H8). Intros H9 H10. + Rewrite (ad_eq_complete ? ? H9). Rewrite (ad_eq_complete ? ? H10). Reflexivity. + Intro H8. Elim (H ? ? ? H4). Intro H9. Elim H9. Intros l2 H10. Elim H10. Intros l3 H11. + Left . Split with (cons x0 l2). Split with l3. Rewrite H11. Reflexivity. + Intro H9. Right . Apply CG_p2. Assumption. + Rewrite H8 in H6. Assumption. + Qed. + +Lemma CG_add_4_2 : (l:(list ad)) (last:ad) (d0:D) + (CG_path cg2 last d0 l) -> (ad_in_list y l)=false -> (CG_path cg1 last d0 l). + Proof. + Induction l. Intros. Inversion H. + Intros a l0. Case l0. Intros. Inversion H0. Rewrite <- H3. Apply CG_p1. Assumption. + Intros. Inversion H0. Rewrite (CG_add_edge_1 a a0) in H7. Elim (orb_false_elim ? ? H1). + Intros H9 H10. Elim (orb_false_elim ? ? H10). + Intros H11 H12. Rewrite H11 in H7. + Rewrite (andb_b_false (ad_eq x a)) in H7. Apply CG_p2. Apply H. Assumption. + Exact H10. + Assumption. + Qed. + +Lemma CG_add_4_3 : (x0:ad) (d0:D) (l:(list ad)) + (ad_list_stutters (cons y l))=false -> + (CG_path cg2 x0 d0 (cons y l)) -> (CG_path cg1 x0 d0 (cons y l)). + Proof. + Intros x0 d0 l. Elim l. Intros. Inversion H0. + Rewrite <- H2. Apply CG_p1. Assumption. + Intros. Inversion H1. Apply CG_p2. Apply CG_add_4_2. + Assumption. + Elim (orb_false_elim ? ? H0). Trivial. + Rewrite (CG_add_edge_1 y a) in H7. + Elim (orb_false_elim ? ? H0). Intros. + Elim (orb_false_elim ? ? H8). Intros. Rewrite H10 in H7. + Rewrite (andb_b_false (ad_eq x y)) in H7. Assumption. + Qed. + +Lemma CG_add_4_4 : (l:(list ad)) (last:ad) (d0:D) + (CG_path cg2 last d0 l) -> (ad_in_list x l)=false -> (CG_path cg1 last d0 l). + Proof. + Induction l. Intros. Inversion H. + Intros a l0. Case l0. Intros. Inversion H0. Rewrite <- H3. Apply CG_p1. Assumption. + Intros. Inversion H0. Apply CG_p2. Apply H. Assumption. + Elim (orb_false_elim ? ? H1). Trivial. + Rewrite (CG_add_edge_1 a a0) in H7. Elim (orb_false_elim ? ? H1). Intros. + Rewrite H8 in H7. Exact H7. + Qed. + +Lemma CG_add_4_5 : (d0:D) (l:(list ad)) + (ad_list_stutters (app l (cons x (nil ad))))=false -> + (CG_path cg2 x d0 (app l (cons x (nil ad)))) -> + (CG_path cg1 x d0 (app l (cons x (nil ad)))). + Proof. + Intros d0 l. Cut {l0:(list ad) & {y0:ad | l=(app l0 (cons y0 (nil ad)))}}+{l=(nil ad)}. + Intro. Elim H. Intro H0. Elim H0. Intros l0 H1. Elim H1. Intros y0 H2 H3 H4. + Rewrite H2 in H4. Rewrite (app_ass l0 (cons y0 (nil ad)) (cons x (nil ad))) in H4. + Simpl in H4. Elim (CG_path_app_3 cg2 l0 (cons x (nil ad)) x y0 d0 H4). Intros d1 H5. + Rewrite H2. Rewrite (app_ass l0 (cons y0 (nil ad)) (cons x (nil ad))). Simpl. + Elim (CG_path_app_2 cg2 l0 (cons x (nil ad)) x y0 d0 H4). Intros d2 H6. + Cut d0=(Dplus d2 d1). Intro. Rewrite H7. + Change (CG_path cg1 x (Dplus d2 d1) (app l0 (app (cons y0 (nil ad)) (cons x (nil ad))))). + Rewrite <- (app_ass l0 (cons y0 (nil ad)) (cons x (nil ad))). + Apply CG_path_app_1 with last:=x x:=y0. Inversion H6. + Inversion H11. Apply CG_p2. + Rewrite <- H15. Apply CG_p1. Assumption. + Rewrite (CG_add_edge_1 y0 x) in H13. Rewrite H2 in H3. + Rewrite (app_ass l0 (cons y0 (nil ad)) (cons x (nil ad))) in H3. Simpl in H3. + Elim (orb_false_elim ? ? (ad_list_stutters_app_conv_r ? ? H3)). Intros. + Elim (orb_false_elim ? ? H17). Intros. + Rewrite (ad_eq_comm y0 x) in H19. + Rewrite H19 in H13. + Rewrite (andb_false_b (ad_eq y x)) in H13. Assumption. + Apply CG_add_4_4. Assumption. + Rewrite H2 in H3. Apply ad_list_stutters_prev_conv_l with l':=(nil ad). Assumption. + Elim (CG_path_weight_and_last_unique cg2 + (app l0 (cons y0 (cons x (nil ad)))) x x d0 (Dplus d2 d1)). + Trivial. + Assumption. + Change (CG_path cg2 x (Dplus d2 d1) (app l0 (app (cons y0 (nil ad)) (cons x (nil ad))))). + Rewrite <- (app_ass l0 (cons y0 (nil ad)) (cons x (nil ad))). + Apply CG_path_app_1 with x:=y0. Assumption. + Assumption. + Intro H0. Rewrite H0. Simpl. Intros. Inversion H2. + Rewrite <- H4. Apply CG_p1. + Assumption. + Elim l. Right . Reflexivity. + Intros. Elim H. Intro H0. Elim H0. Intros l1 H1. Elim H1. Intros a0 H2. Rewrite H2. + Left . Split with (cons a l1). Split with a0. Reflexivity. + Intro H0. Rewrite H0. Left . Split with (nil ad). Split with a. Reflexivity. + Qed. + +(*s If there is no cycle of negative weight in the old graph [cg1], and the distance + from [y] to [x] is $\geq -d$, then there is no simple cycle of negative weight in + the new graph [cg2] either: *) + +Lemma CG_add_4 : + ((x0:ad) (d0:D) (l:(list ad)) (CG_path cg1 x0 d0 (cons x0 l)) -> (Dle Dz d0)=true) -> + (Ddle (SOME ? (Dneg d)) (ad_simple_path_dist cg1 y x))=true -> + (x0:ad) (d0:D) (l:(list ad)) (CG_path cg2 x0 d0 (cons x0 l)) -> + (ad_list_stutters l)=false -> (Dle Dz d0)=true. + Proof. + Intros. Elim (CG_add_4_1 ? ? ? ? H1). Intro H3. Elim H3. Intros l0 H4. Elim H4. + Intros l1 H5. Rewrite H5 in H1. + Change (CG_path cg2 x0 d0 (app l0 (app (cons x (nil ad)) (cons y l1)))) in H1. + Elim (CG_path_app_4 cg2 ? ? ? ? ? H1). Intros d1 H6. Elim H6. Intros d2 H7. + Elim H7. Intros H8 H9. Elim H8. Intros H10 H11. Clear H3 H6 H7 H8. Rewrite H9. + Inversion_clear H11. Rewrite (CG_add_edge_1 x y) in H6. Rewrite (ad_eq_correct x) in H6. + Rewrite (ad_eq_correct y) in H6. Simpl in H6. Apply Dplus_reg_r with d'':=(Dneg d1). + Rewrite Dplus_assoc. Rewrite Dplus_neg. Rewrite Dplus_d_z. Rewrite Dplus_z_d. + Apply Dplus_reg_l with d'':=d1. Rewrite Dplus_neg. Rewrite <- Dplus_assoc. + Change (cons x0 l)=(app l0 (app (cons x (nil ad)) (cons y l1))) in H5. + Rewrite (ass_app l0 (cons x (nil ad)) (cons y l1)) in H5. + Cut {l'0:(list ad) | (app l0 (cons x (nil ad)))=(cons x0 l'0)}. Intro H7. Elim H7. + Intros l'0 H8. Clear H4 H7. Rewrite H8 in H5. Simpl in H5. Inversion H5. Rewrite H8 in H10. + Cut (CG_path cg1 x (Dplus d1 d3) (cons y (app l1 l'0))). Intro. + Elim (option_sum ? (CG_edge cg1 x y)). Intro H11. Elim H11. Intros d'0 H12. + Rewrite H12 in H6. Inversion_clear H6. Elim (Dmin_choice d d'0). Intro H13. Rewrite H13. + Apply Dplus_reg_r with d'':=(Dneg d). Rewrite Dplus_assoc. Rewrite Dplus_neg. + Rewrite Dplus_d_z. Rewrite Dplus_z_d. + Change (Ddle (SOME D (Dneg d)) (SOME D (Dplus d1 d3)))=true. + Apply Ddle_trans with dd':=(ad_simple_path_dist cg1 y x). Assumption. + Exact (ad_simple_path_dist_correct cg1 H y x ? ? H4). + Intro H13. Rewrite H13. Apply (H x (Dplus (Dplus d1 d3) d'0) (cons y (app l1 l'0))). + Apply (CG_path_app_1 cg1 (cons x (cons y (nil ad))) (app l1 l'0) x y). Assumption. + Rewrite <- (Dplus_z_d d'0). Apply CG_p2. Apply CG_p1. Reflexivity. + Assumption. + Intro H11. Rewrite H11 in H6. Inversion H6. Rewrite <- H13. + Apply Dplus_reg_r with d'':=(Dneg d). Rewrite Dplus_assoc. Rewrite Dplus_neg. + Rewrite Dplus_d_z. Rewrite Dplus_z_d. + Change (Ddle (SOME D (Dneg d)) (SOME D (Dplus d1 d3)))=true. + Apply Ddle_trans with dd':=(ad_simple_path_dist cg1 y x). Assumption. + Exact (ad_simple_path_dist_correct cg1 H y x ? ? H4). + Apply (CG_path_app_1 cg1 (cons y l1) l'0 x x0). Rewrite <- H8. Apply CG_add_4_5. + Rewrite H8. Elim (CG_path_last cg2 ? ? ? H3). Intros l'1 H11. Rewrite H7 in H2. + Simpl. Rewrite (ad_list_stutters_app_conv_l ? ? H2). Rewrite H11 in H2. + Rewrite (ass_app l'0 l'1 (cons x0 (nil ad))) in H2. + Elim (sumbool_of_bool (ad_in_list x0 l'0)). Intro H12. + Rewrite (ad_list_stutters_prev_l ? (nil ad) ? (ad_in_list_l l'0 l'1 x0 H12)) in H2. + Discriminate H2. + Intro H12. Rewrite H12. Reflexivity. + Rewrite H8. Assumption. + Apply CG_add_4_3. Rewrite H7 in H2. Exact (ad_list_stutters_app_conv_r l'0 (cons y l1) H2). + Assumption. + Generalize H5. Elim l0. Simpl. Intro H7. Exists (nil ad). Inversion_clear H7. Reflexivity. + Intros. Rewrite (app_ass (cons a l2) (cons x (nil ad)) (cons y l1)) in H8. Simpl in H8. + Exists (app l2 (cons x (nil ad))). Inversion_clear H8. Reflexivity. + Intro H3. Exact (H x0 d0 l H3). + Qed. + +Lemma CG_add_5_1 : (n:nat) + ((x0:ad) (d0:D) (l:(list ad)) (CG_path cg1 x0 d0 (cons x0 l)) -> (Dle Dz d0)=true) -> + (Ddle (SOME ? (Dneg d)) (ad_simple_path_dist cg1 y x))=true -> + (x0:ad) (d0:D) (l:(list ad)) (CG_path cg2 x0 d0 (cons x0 l)) -> + (le (length l) n) -> (Dle Dz d0)=true. + Proof. + Induction n. Induction l. Intros. Inversion H1. Apply Dle_refl. + Intros. Elim (le_Sn_O ? H3). + Intros. Elim (sumbool_of_bool (ad_list_stutters l)). Intros H4. + Elim (ad_list_stutters_has_circuit l H4). Intros y0 H5. Elim H5. Intros l0 H6. Elim H6. + Intros l1 H7. Elim H7. Intros l2 H8. Rewrite H8 in H2. + Elim (CG_path_app_4 cg2 (cons x0 l0) (app l1 (cons y0 l2)) x0 y0 d0 H2). Intros d1 H9. + Elim H9. Intros d2 H10. Elim H10. Intros H11 H12. Elim H11. Intros H13 H14. + Clear H5 H6 H7 H9 H10 H11. Elim (CG_path_app_4 cg2 (cons y0 l1) l2 x0 y0 d2 H14). + Intros d3 H5. Elim H5. Intros d4 H6. Elim H6. Intros H7 H9. Elim H7. Intros H10 H11. + Clear H5 H6 H7 H14. Rewrite H12. Rewrite H9. Apply Dle_trans with d':=(Dplus d4 d1). + Apply (H H0 H1 x0 (Dplus d4 d1) (app l0 (cons y0 l2))). + Cut (cons x0 (app l0 (cons y0 l2)))=(app (app (cons x0 l0) (cons y0 (nil ad))) l2). + Intro. Rewrite H5. Exact (CG_path_app_1 cg2 ? ? ? ? ? ? H11 H13). + Exact (ass_app (cons x0 l0) (cons y0 (nil ad)) l2). + Rewrite ad_list_app_length. Apply le_S_n. Apply le_trans with m:=(length l). + Rewrite H8. Rewrite ad_list_app_length. Simpl. Rewrite ad_list_app_length. Simpl. + Rewrite <- plus_Snm_nSm. Rewrite <- plus_Snm_nSm. Rewrite <- plus_Snm_nSm. Simpl. + Rewrite <- plus_Snm_nSm. Simpl. Apply le_n_S. Apply le_n_S. Apply le_reg_l. + Apply le_plus_r. Assumption. + Apply Dle_plus_mono. Apply Dle_trans with (Dplus d4 Dz). Rewrite Dplus_d_z. Apply Dle_refl. + Apply Dle_plus_mono. Apply Dle_refl. + Apply (H H0 H1 y0 d3 (app l1 (cons y0 (nil ad))) H10). Rewrite ad_list_app_length. Simpl. + Apply le_S_n. Apply le_trans with m:=(length l). Rewrite H8. Rewrite ad_list_app_length. + Simpl. Rewrite ad_list_app_length. Simpl. Rewrite <- plus_Snm_nSm. Rewrite <- plus_Snm_nSm. + Rewrite <- plus_Snm_nSm. Simpl. Rewrite <- plus_Snm_nSm. Simpl. Apply le_n_S. Apply le_n_S. + Apply le_trans with m:=(plus (length l1) (length l2)). Apply le_plus_plus. Apply le_n. + Apply le_O_n. Apply le_plus_r. Assumption. + Apply Dle_refl. + Intro H4. Exact (CG_add_4 H0 H1 x0 d0 l H2 H4). + Qed. + +Lemma CG_add_5 : + ((x0:ad) (d0:D) (l:(list ad)) (CG_path cg1 x0 d0 (cons x0 l)) -> (Dle Dz d0)=true) -> + (Ddle (SOME ? (Dneg d)) (ad_simple_path_dist cg1 y x))=true -> + (x0:ad) (d0:D) (l:(list ad)) (CG_path cg2 x0 d0 (cons x0 l)) -> (Dle Dz d0)=true. + Proof. + Intros. Exact (CG_add_5_1 (length l) H H0 x0 d0 l H1 (le_n ?)). + Qed. + + End CGAdd. + +(*s Properties of the range of the graph *) + +Definition cg_range := (DMerge D). + +Lemma cg_range_1 + : (cg:CGraph1) (x,y:ad) (d:D) + (CG_edge cg x y)=(SOME ? d) -> (in_dom D y (cg_range cg))=true. + Proof. + Unfold cg_range CG_edge. Intros. Elim (option_sum ? (MapGet ? cg x)). Intro H0. Elim H0. + Intros edges H1. Rewrite H1 in H. Apply in_dom_DMerge_3 with a:=x m0:=edges. Assumption. + Unfold in_dom. Generalize H. Case (MapGet D edges y). Intro H2. Discriminate H2. + Trivial. + Intro H0. Rewrite H0 in H. Discriminate H. + Qed. + +Lemma cg_range_2 + : (cg:CGraph1) (y:ad) (in_dom D y (cg_range cg))=true -> + {x:ad & {d:D | (CG_edge cg x y)=(SOME ? d)}}. + Proof. + Intros. Elim (in_dom_DMerge_2 ? cg y H). Intros x H0. Elim H0. Intros edges H1. Elim H1. + Intros H2 H3. Split with x. Elim (in_dom_some ? edges y H3). Intros d H4. Split with d. + Unfold CG_edge. Rewrite H2. Rewrite H4. Reflexivity. + Qed. + +Lemma cg_range_4 : (cg:CGraph1) (x,y:ad) (d:D) (a:ad) + (in_dom D a (cg_range (CG_add cg x y d)))=(orb (ad_eq a y) (in_dom D a (cg_range cg))). + Proof. + Intros. Elim (sumbool_of_bool (in_dom D a (cg_range (CG_add cg x y d)))). Intro H. + Elim (cg_range_2 ? ? H). Intros a0 H0. Elim H0. Intros d0 H1. Clear H0. + Change (CG_edge (cg2 cg x y d) a0 a)=(SOME D d0) in H1. + Rewrite (CG_add_edge_1 cg x y d a0 a) in H1. Rewrite H. + Elim (sumbool_of_bool (andb (ad_eq x a0) (ad_eq y a))). Intro H2. Elim (andb_prop ? ? H2). + Intros H3 H4. Rewrite (ad_eq_comm y a) in H4. Rewrite H4. Reflexivity. + Intro H2. Rewrite H2 in H1. Rewrite (cg_range_1 ? ? ? ? H1). Apply sym_eq. Apply orb_b_true. + Intro H. Rewrite H. Elim (sumbool_of_bool (ad_eq a y)). Intro H0. + Rewrite (ad_eq_complete ? ? H0) in H. Cut {d0:D | (CG_edge (cg2 cg x y d) x y)=(SOME ? d0)}. + Intro H1. Elim H1. Intros d0 H2. Unfold cg2 in H2. Rewrite (cg_range_1 ? ? ? ? H2) in H. + Discriminate H. + Rewrite (CG_add_edge_1 cg x y d x y). Rewrite (ad_eq_correct x). Rewrite (ad_eq_correct y). + Case (CG_edge cg x y). Split with d. Reflexivity. + Intro d0. Split with (Dmin d d0). Reflexivity. + Intro H0. Rewrite H0. Elim (sumbool_of_bool (in_dom D a (cg_range cg))). Intro H1. + Elim (cg_range_2 ? ? H1). Intros a0 H2. Elim H2. Intros d0 H3. + Cut {d1:D | (CG_edge (cg2 cg x y d) a0 a)=(SOME ? d1)}. Intro H4. Elim H4. Intros d1 H5. + Unfold cg2 in H5. Rewrite (cg_range_1 ? ? ? ? H5) in H. Discriminate H. + Rewrite (CG_add_edge_1 cg x y d a0 a). Rewrite (ad_eq_comm a y) in H0. Rewrite H0. + Rewrite (andb_b_false (ad_eq x a0)). Split with d0. Assumption. + Intro H1. Rewrite H1. Reflexivity. + Qed. + +Lemma cg_out_of_range_1 : (cg:CGraph1) (y:ad) (in_dom D y (cg_range cg))=false -> + (x:ad) (CG_edge cg x y)=(NONE D). + Proof. + Intros. Elim (option_sum ? (CG_edge cg x y)). Intro H0. Elim H0. Intros d H1. + Rewrite (cg_range_1 cg x y d H1) in H. Discriminate H. + Trivial. + Qed. + +Lemma cg_out_of_range_2 : (cg:CGraph1) (y:ad) (in_dom D y (cg_range cg))=false -> + (x:ad) (ad_eq x y)=false -> (ad_simple_path_dist cg x y)=(NONE D). + Proof. + Intros. Elim (option_sum ? (ad_simple_path_dist cg x y)). Intro H1. Elim H1. Intros d H2. + Elim (ad_simple_path_dist_complete_2 cg x y d H2). Intros l H3. + Cut {a:ad & {d':D | (CG_edge cg a y)=(SOME ? d')}}. Intro H4. Elim H4. Intros a H5. Elim H5. + Intros d' H6. Rewrite (cg_out_of_range_1 cg y H a) in H6. Discriminate H6. + Generalize x H0 d H3. Elim l. Intros. Inversion H5. + Rewrite H8 in H4. + Rewrite (ad_eq_correct y) in H4. Discriminate H4. + Intros. Inversion H6. Elim (sumbool_of_bool (ad_eq a y)). + Intro H14. Split with x0. + Split with d'. Rewrite <- (ad_eq_complete ? ? H14). Assumption. + Intro H14. Exact (H4 a H14 ? H10). + Trivial. + Qed. + +Lemma cg_out_of_range_3 : (cg:CGraph1) (y:ad) (in_dom D y (cg_range cg))=false -> + (x:ad) (ad_eq x y)=false -> (CG_leq cg x y)=false. + Proof. + Intros. Unfold CG_leq. Rewrite (cg_out_of_range_2 cg y H x H0). Reflexivity. + Qed. + +Lemma cg_add_out_of_range_1 : (cg:(CGraph1)) (x,y:ad) (d:D) + ((x0:ad) (d0:D) (l:(list ad)) (CG_path cg x0 d0 (cons x0 l)) -> (Dle Dz d0)=true) -> + (in_dom D x (cg_range cg))=false -> + (ad_eq y x)=false -> + (x0:ad) (d0:D) (l:(list ad)) (CG_path (CG_add cg x y d) x0 d0 (cons x0 l)) -> + (Dle Dz d0)=true. + Proof. + Intros. Apply (CG_add_5 cg x y d H) with x0:=x0 l:=l. + Rewrite (cg_out_of_range_2 cg x H0 y H1). Reflexivity. + Assumption. + Qed. + + +Lemma cg_add_dom_subset : (cg:CGraph1) (x,y:ad) (d:D) + (MapSubset ? ? (MapDom ? cg) (MapDom ? (CG_add cg x y d))). + Proof. + Unfold CG_add. Intros. Elim (option_sum ? (MapGet ? cg x)). Intro H. Elim H. Intros edges H0. + Rewrite H0. Elim (option_sum ? (MapGet D edges y)). Intro H1. Elim H1. Intros d0 H2. + Rewrite H2. Apply MapSubset_Dom_1. Apply MapSubset_Put. + Intro H1. Rewrite H1. Apply MapSubset_Dom_1. Apply MapSubset_Put. + Intro H. Rewrite H. Apply MapSubset_Dom_1. Apply MapSubset_Put. + Qed. + +(*s Adding a lis of adresses connected to [root] with weight $0$ *) + +Fixpoint CG_add_root [root:ad; cg:CGraph1; l:(list ad)] : CGraph1 := + Cases l of + nil => cg + | (cons x l') => (CG_add_root root (CG_add cg root x Dz) l') + end. + +Lemma CG_add_root_out_of_range : (l:(list ad)) (cg:CGraph1) (root:ad) + ((x0:ad) (d0:D) (l:(list ad)) (CG_path cg x0 d0 (cons x0 l)) -> (Dle Dz d0)=true) -> + (MapSubset ? ? (Elems l) (MapDom ? cg)) -> + (ad_in_list root l)=false -> + (in_dom ? root (cg_range cg))=false -> + (x0:ad) (d0:D) (l0:(list ad)) (CG_path (CG_add_root root cg l) x0 d0 (cons x0 l0)) -> + (Dle Dz d0)=true. + Proof. + Induction l. Trivial. + Simpl. Intros. Apply (H (CG_add cg root a Dz) root) with x0:=x0 d0:=d0 l1:=l1. Intros. + Apply (cg_add_out_of_range_1 cg root a Dz) with x0:=x1 d0:=d1 l:=l2. Intros. + Exact (H0 ? ? ? H6). + Assumption. + Elim (orb_false_elim ? ? H2). Intros. Rewrite ad_eq_comm. Assumption. + Assumption. + Apply MapSubset_trans with m':=(MapPut unit (Elems l0) a tt). Apply MapSubset_Put. + Apply MapSubset_trans with m':=(MapDom ? cg). Assumption. + Apply cg_add_dom_subset. + Elim (orb_false_elim ? ? H2). Trivial. + Rewrite cg_range_4. Elim (orb_false_elim ? ? H2). Intros H5 H6. Rewrite H5. Rewrite H3. + Reflexivity. + Assumption. + Qed. + +Lemma CG_add_rooted_1 : (cg:CGraph1) (root,a:ad) (d:D) + (CG_edge cg root a)=(NONE D) -> + (CG_edge (CG_add cg root a d) root a)=(SOME D d). + Proof. + Intros. Change (CG_edge (cg2 cg root a d) root a)=(SOME D d). Rewrite CG_add_edge_1. + Rewrite (ad_eq_correct root). Rewrite (ad_eq_correct a). Rewrite H. Reflexivity. + Qed. + +Lemma CG_add_root_rooted_1 : (l:(list ad)) (cg:CGraph1) (root,a:ad) + (ad_list_stutters l)=false -> + (ad_in_list a l)=false -> (d:D) (CG_edge cg root a)=(SOME D d) -> + (CG_edge (CG_add_root root cg l) root a)=(SOME D d). + Proof. + Induction l. Trivial. + Simpl. Intros. Elim (orb_false_elim ? ? H0). Intros. Elim (orb_false_elim ? ? H1). + Intros. Apply H. Assumption. + Assumption. + Change (CG_edge (cg2 cg root a Dz) root a0)=(SOME D d). Rewrite CG_add_edge_1. + Rewrite (ad_eq_comm a a0). Rewrite H5. Rewrite (andb_b_false (ad_eq root root)). Assumption. + Qed. + +Lemma CG_add_root_rooted_2 : (l:(list ad)) (cg:CGraph1) (root:ad) + (ad_list_stutters l)=false -> + ((a0:ad) (ad_in_list a0 l)=true -> (CG_edge cg root a0)=(NONE D)) -> + (a:ad) (ad_in_list a l)=true -> + (CG_edge (CG_add_root root cg l) root a)=(SOME ? Dz). + Proof. + Induction l. Intros. Discriminate H1. + Simpl. Intros. Elim (orb_false_elim ? ? H0). Intros. Elim (sumbool_of_bool (ad_eq a0 a)). + Intro H5. Rewrite (ad_eq_complete ? ? H5). Apply CG_add_root_rooted_1. Assumption. + Assumption. + Apply CG_add_rooted_1. Apply H1. Rewrite (ad_eq_correct a). Reflexivity. + Intro H5. Rewrite H5 in H2. Simpl in H2. Apply H. Assumption. + Intros. Change (CG_edge (cg2 cg root a Dz) root a1)=(NONE D). Rewrite CG_add_edge_1. + Elim (sumbool_of_bool (ad_eq a a1)). Intro H7. Rewrite (ad_eq_complete ? ? H7) in H3. + Rewrite H6 in H3. Discriminate H3. + Intro H7. Rewrite H7. Rewrite (andb_b_false (ad_eq root root)). + Apply H1. Rewrite H6. Apply orb_b_true. + Assumption. + Qed. + +Lemma CG_add_root_rooted_3 : (cg:CGraph1) (root:ad) + (in_dom ? root cg)=false -> + (a:ad) (in_dom ? a cg)=true -> + (CG_edge (CG_add_root root cg (ad_list_of_dom ? cg)) root a)=(SOME ? Dz). + Proof. + Intros. Apply CG_add_root_rooted_2. Apply ad_list_of_dom_not_stutters. + Intros. Unfold CG_edge. Rewrite (in_dom_none ? ? ? H). Reflexivity. + Rewrite ad_in_list_of_dom_in_dom. Assumption. + Qed. + +Lemma CG_add_root_rooted_4 : (l:(list ad)) (cg:CGraph1) (root:ad) (a:ad) + (in_dom ? a (CG_add_root root cg l))=true -> {a=root}+{(in_dom ? a cg)=true}. + Proof. + Induction l. Intros. Right . Exact H. + Simpl. Intros. Elim (H (CG_add cg root a Dz) root a0 H0). Intro H1. Left . Assumption. + Intro H1. Unfold in_dom CG_add in H1. Elim (option_sum ? (MapGet ? cg root)). Intro H2. + Elim H2. Intros edges H3. Rewrite H3 in H1. Elim (option_sum ? (MapGet D edges a)). Intro H4. + Elim H4. Intros d H5. Rewrite H5 in H1. + Rewrite (MapPut_semantics ? cg root (MapPut D edges a (Dmin Dz d)) a0) in H1. + Elim (sumbool_of_bool (ad_eq root a0)). Intro H6. Left . Rewrite (ad_eq_complete ? ? H6). + Reflexivity. + Intro H6. Rewrite H6 in H1. Right . Exact H1. + Intro H4. Rewrite H4 in H1. + Rewrite (MapPut_semantics ? cg root (MapPut D edges a Dz) a0) in H1. + Elim (sumbool_of_bool (ad_eq root a0)). Intro H5. Left . Rewrite (ad_eq_complete ? ? H5). + Reflexivity. + Intro H5. Rewrite H5 in H1. Right . Exact H1. + Intro H2. Rewrite H2 in H1. Rewrite (MapPut_semantics ? cg root (M1 D a Dz) a0) in H1. + Elim (sumbool_of_bool (ad_eq root a0)). Intro H3. Left . Rewrite (ad_eq_complete ? ? H3). + Reflexivity. + Intro H3. Rewrite H3 in H1. Right . Exact H1. + Qed. + +Lemma CG_edge_dist_some_1 : (n:nat) (cg:CGraph1) (x,y:ad) (d:D) (prefix:(list ad)) + (CG_edge cg x y)=(SOME D d) -> (ad_in_list y prefix)=false -> + {d':D | (Ddle (ad_simple_path_dist_1 cg x y prefix (S n)) (SOME ? d'))=true}. + Proof. + Unfold CG_edge. Intros. Simpl. Elim (sumbool_of_bool (ad_eq x y)). Intro H1. Rewrite H1. + Split with Dz. Simpl. Apply Dle_refl. + Intro H1. Rewrite H1. Elim (option_sum ? (MapGet ? cg x)). Intro H2. Elim H2. + Intros edges H3. Rewrite H3 in H. Rewrite H3. Elim (option_sum ? (MapGet D edges y)). + Intro H4. Elim H4. Intros d0 H5. Rewrite H5 in H. Inversion H. Split with (Dplus Dz d). + Rewrite H7 in H5. Apply Ddle_trans with dd':=([z:ad] [d0:D] + Case (orb (ad_eq z x) (ad_in_list z prefix)) of + (NONE D) + (Ddplus + (ad_simple_path_dist_1 cg z y (cons x prefix) n) d0) + end y d). + Apply all_min_le_1 with f:=[z:ad] [d0:D] + Case (orb (ad_eq z x) (ad_in_list z prefix)) of + (NONE D) + (Ddplus (ad_simple_path_dist_1 cg z y (cons x prefix) n) + d0) + end. + Assumption. + Rewrite (ad_eq_comm y x). Rewrite H1. Rewrite H0. Simpl. Case n. Simpl. + Rewrite (ad_eq_correct y). Apply Ddle_refl. + Intro. Simpl. Rewrite (ad_eq_correct y). Apply Ddle_refl. + Intro H4. Rewrite H4 in H. Discriminate H. + Intro H2. Rewrite H2 in H. Discriminate H. + Qed. + +Lemma CG_edge_dist_some : (cg:CGraph1) (x,y:ad) (d:D) + (CG_edge cg x y)=(SOME D d) -> {d':D | (ad_simple_path_dist cg x y)=(SOME ? d')}. + Proof. + Intros. Elim (option_sum ? (ad_simple_path_dist cg x y)). Trivial. + Unfold ad_simple_path_dist. Intro H0. Elim (option_sum ? (MapGet ? cg x)). Intro H1. Elim H1. + Intros edges H2. Elim (MapCard_is_not_O ? cg x edges H2). Intros n H3. + Elim (CG_edge_dist_some_1 n cg x y d (nil ad) H (refl_equal ? ?)). Intros d0 H4. + Rewrite H3 in H0. Rewrite H0 in H4. Discriminate H4. + Intro H1. Unfold CG_edge in H. Rewrite H1 in H. Discriminate H. + Qed. + +Lemma CG_add_root_rooted : (cg:CGraph1) (root:ad) + ((x:ad) (d:D) (l:(list ad)) (CG_path cg x d (cons x l)) -> (Dle Dz d)=true) -> + (in_dom ? root cg)=false -> + (a:ad) (in_dom ? a (CG_add_root root cg (ad_list_of_dom ? cg)))=true -> + (CG_leq (CG_add_root root cg (ad_list_of_dom ? cg)) root a)=true. + Proof. + Intros. Elim (CG_add_root_rooted_4 ? ? ? ? H1). Intro H2. Rewrite H2. Apply CG_leq_refl. + Intro H2. Elim (CG_edge_dist_some ? root a Dz (CG_add_root_rooted_3 cg root H0 a H2)). + Intros d H3. Unfold CG_leq. Rewrite H3. Reflexivity. + Qed. + +Lemma CG_add_sat : (cg:CGraph1) (root,a:ad) (d:D) (rho:ad->D) + (CGsat (cg2 cg root a d) rho) -> (CGsat cg rho). + Proof. + Unfold CGsat. Intros. Elim (sumbool_of_bool (andb (ad_eq root x) (ad_eq a y))). Intro H1. + Apply Dle_trans with d':=(Dplus (rho y) (Dmin d d0)). Apply H. Rewrite CG_add_edge_1. + Rewrite H1. Rewrite H0. Reflexivity. + Apply Dle_plus_mono. Apply Dle_refl. + Apply Dmin_le_2. + Intro H1. Apply H. Rewrite CG_add_edge_1. Rewrite H1. Assumption. + Qed. + +Lemma CG_add_root_sat : (l:(list ad)) (cg:CGraph1) (root:ad) (rho:ad->D) + (CGsat (CG_add_root root cg l) rho) -> (CGsat cg rho). + Proof. + Induction l. Trivial. + Simpl. Intros. Apply (CG_add_sat cg root a Dz rho). Unfold cg2. Exact (H ? ? ? H0). + Qed. + +Lemma CG_add_root_consistent : (l:(list ad)) (cg:CGraph1) (root:ad) + (CGconsistent (CG_add_root root cg l)) -> (CGconsistent cg). + Proof. + Unfold CGconsistent. Intros. Elim H. Intros rho H0. Split with rho. + Exact (CG_add_root_sat l cg root rho H0). + Qed. + +Lemma CG_circuit_complete_1 : (cg:CGraph1) + ((x:ad)(d:D)(l:(list ad)) + (CG_path cg x d (cons x l)) -> (Dle Dz d)=true) -> + (root:ad) + root=(ad_alloc_opt unit (FSetUnion (MapDom ? cg) (MapDom ? (cg_range cg)))) -> + (cg':CGraph1) cg'=(CG_add_root root cg (ad_list_of_dom ? cg)) + -> (CGconsistent cg). + Proof. + Intros. Apply (CG_add_root_consistent (ad_list_of_dom (Map D) cg) cg root). Rewrite <- H1. + Cut (orb (in_dom ? root cg) (in_dom ? root (cg_range cg)))=false. Intro H2. + Elim (orb_false_elim ? ? H2). Intros. Elim CG_rooted_sat with cg:=cg' root:=root d0:=Dz. + Intros rho H5. Elim H5. Unfold CGconsistent. Intros H6 H7. Split with rho. Assumption. + Rewrite H1. Intros. + Apply CG_add_root_out_of_range with l:=(ad_list_of_dom (Map D) cg) cg:=cg root:=root + x0:=x d0:=d l0:=l. + Assumption. + Apply MapSubset_2_imp. Unfold MapSubset_2. + Apply eqmap_trans with m':=(MapDomRestrBy unit unit (MapDom (Map D) cg) (MapDom (Map D) cg)). + Apply MapDomRestrBy_ext. Apply Elems_of_list_of_dom. + Apply eqmap_refl. + Apply MapDomRestrBy_m_m_1. + Rewrite ad_in_list_of_dom_in_dom. Assumption. + Assumption. + Assumption. + Intros. Rewrite H1. Apply CG_add_root_rooted. Assumption. + Assumption. + Rewrite <- H1. Assumption. + Rewrite MapDom_Dom. Rewrite MapDom_Dom. Rewrite <- in_FSet_union. Rewrite H0. + Unfold in_FSet. Apply ad_alloc_opt_allocates. + Qed. + +(*s If there is no circuit [(cons x l)] with negative weight [d], then [cg] is consistent: *) + +Theorem CG_circuit_complete : (cg:CGraph1) + ((x:ad) (d:D) (l:(list ad)) (CG_path cg x d (cons x l)) -> (Dle Dz d)=true) -> + (CGconsistent cg). + Proof. + Intros. EApply CG_circuit_complete_1. Assumption. + Reflexivity. + Reflexivity. + Qed. + +Lemma CG_translate_l : (cg:CGraph1) (rho:ad->D) (d:D) (CGsat cg rho) -> + (CGsat cg [a:ad] (Dplus d (rho a))). + Proof. + Unfold CGsat. Intros. Rewrite Dplus_assoc. Apply Dle_plus_mono. Apply Dle_refl. + Apply H. Assumption. + Qed. + +(*s [(CGconsistent_anchored cg a d)] if there exists a valuation $\rho$ which + satisfies [cg] and such that $\rho(a)=d$ +*) + +Definition CGconsistent_anchored := + [cg:CGraph1][a:ad][d0:D] {rho:ad->D | (CGsat cg rho) /\ (rho a)=d0}. + +Lemma CGconsistent_then_anchored + : (cg:CGraph1) (CGconsistent cg) -> + (a:ad) (d0:D) (CGconsistent_anchored cg a d0). + Proof. + Unfold CGconsistent CGconsistent_anchored. Intros. Elim H. Intros rho H0. + Split with [a0:ad](Dplus (Dplus d0 (Dneg (rho a))) (rho a0)). Split. + Apply CG_translate_l. Assumption. + Rewrite Dplus_assoc. Rewrite Dplus_neg_2. Apply Dplus_d_z. + Qed. + +Lemma CGanchored_then_consistent : (cg:CGraph1) (a:ad) (d0:D) (CGconsistent_anchored cg a d0) -> + (CGconsistent cg). + Proof. + Unfold CGconsistent CGconsistent_anchored. Intros. Elim H. Intros rho H0. Elim H0. Intros. + Split with rho. Assumption. + Qed. + +(*s Definition of [ad_0_path_dist_1] + a more efficient version of [ad_simple_path_dist]: *) + +Section CGDist1. + + Variable cg : CGraph1. + +Fixpoint ad_0_path_dist_1 [x,y:ad; l:(list ad); n:nat] : (option D) := + if (ad_eq x y) + then (SOME ? Dz) + else + Cases n of + O => (NONE ?) + | (S n') => Cases (MapGet ? cg x) of + NONE => (NONE ?) + | (SOME edges) => + if (ad_in_list x l) + then (NONE D) + else let l'=(cons x l) in (* builds reverse path *) + (all_min [z:ad][d:D] + if (ad_in_list z l') + then (NONE D) + else (Ddplus (ad_0_path_dist_1 z y l' n') d) + edges) + end + end. + +Definition ad_0_path_dist := [x,y:ad] + (ad_0_path_dist_1 x y (nil ad) (MapCard ? cg)). + +Lemma ad_0_path_dist_1_ge : (n:nat) (l:(list ad)) (x,y:ad) + (Ddle (ad_simple_path_dist_1 cg x y l n) (ad_0_path_dist_1 x y l n))=true. + Proof. + Induction n. Simpl. Intros. Apply Ddle_refl. + Simpl. Intros. Case (ad_eq x y). Apply Ddle_refl. + Case (MapGet ? cg x). Apply Ddle_refl. + Intro. Case (ad_in_list x l). Apply Ddle_d_none. + Apply all_min_le_3. Intros. Case (orb (ad_eq a x) (ad_in_list a l)). Apply Ddle_refl. + Apply Ddle_plus_mono. Apply H. + Apply Dle_refl. + Qed. + +Lemma ad_0_path_dist_1_correct_1 : + ((x:ad) (d:D) (l:(list ad)) (CG_path cg x d (cons x l)) -> (Dle Dz d)=true) -> + (n:nat) (x,y:ad) (l:(list ad)) (d:D) + (le (length l) n) -> (CG_path cg y d (cons x l)) -> + (prefix:(list ad)) + (ad_list_stutters (app (rev prefix) (cons x l)))=false -> + (Ddle (ad_0_path_dist_1 x y prefix n) (SOME ? d))=true. + Proof. + Induction n. Intros x y l. Case l. Intros. Simpl. + Inversion H1. Rewrite H5. + Rewrite (ad_eq_correct y). Apply Ddle_refl. + Intros. Elim (le_Sn_O ? H0). + Intros n0 H0 x y l. Case l. Intros. Inversion H2. + Rewrite H6. Simpl. + Rewrite (ad_eq_correct y). Rewrite H5. Apply Ddle_refl. + Intros. Simpl. Elim (sumbool_of_bool (ad_eq x y)). Intro H4. Rewrite H4. + Rewrite (ad_eq_complete ? ? H4) in H2. Exact (H ? ? ? H2). + + Intro H4. Rewrite H4. Elim (option_sum ? (MapGet ? cg x)). Intro H5. Elim H5. + Intros edges H6. Rewrite H6. Inversion_clear H2. Apply Ddle_trans + with dd':=Case (ad_in_list a (cons x prefix)) of + (NONE D) + (Ddplus (ad_0_path_dist_1 a y (cons x prefix) n0) d') + end. + Cut (MapGet ? edges a)=(SOME ? d'). Intro. Cut (ad_in_list x prefix)=false. Intro H9. + Rewrite H9. Exact (all_min_le_1 [z:ad] [d:D] + Case (orb (ad_eq z x) (ad_in_list z prefix)) of + (NONE D) + (Ddplus (ad_0_path_dist_1 z y (cons x prefix) n0) d) + end edges a d' H2). + Rewrite <- ad_in_list_rev. Exact (ad_list_stutters_prev_conv_l ? ? ? H3). + Unfold CG_edge in H8. Rewrite H6 in H8. Elim (option_sum ? (MapGet D edges a)). + Intro H9. Elim H9. Intros d1 H10. Rewrite H10 in H8. Rewrite H10. Assumption. + Intro H9. Rewrite H9 in H8. Discriminate H8. + Rewrite (ad_list_app_rev prefix (cons a l0) x) in H3. + Rewrite <- (ad_in_list_rev (cons x prefix) a). + Rewrite (ad_list_stutters_prev_conv_l ? ? ? H3). + Apply (Ddle_plus_mono (ad_0_path_dist_1 a y (cons x prefix) n0) (SOME D d0) d' d'). + Exact (H0 a y l0 d0 (le_S_n ? ? H1) H7 (cons x prefix) H3). + Apply Dle_refl. + Intro H5. Inversion H2. + Unfold CG_edge in H11. Rewrite H5 in H11. Discriminate H11. + Qed. + +Lemma ad_0_path_dist_1_le : + ((x:ad) (d:D) (l:(list ad)) (CG_path cg x d (cons x l)) -> (Dle Dz d)=true) -> + (n:nat) (x,y:ad) + (Ddle (ad_0_path_dist_1 x y (nil ad) n) (ad_simple_path_dist_1 cg x y (nil ad) n))=true. + Proof. + Intros. Elim (option_sum ? (ad_simple_path_dist_1 cg x y (nil ad) n)). Intro H0. Elim H0. + Intros d H1. Rewrite H1. + Elim (ad_simple_path_dist_1_complete_1 cg n x y (nil ad) Dz) with d0:=d. Intros l H2. + Elim H2. Intros H3 H4. Apply (ad_0_path_dist_1_correct_1 H n x y l). Exact (proj2 ? ? H4). + Rewrite (Dplus_d_z d) in H3. Exact H3. + Exact (proj1 ? ? H4). + Simpl. Apply CG_p1. Reflexivity. + Reflexivity. + Assumption. + Intro H0. Rewrite H0. Apply Ddle_d_none. + Qed. + +Lemma ad_0_path_dist_correct_1 : + (CGconsistent cg) -> + (x,y:ad) (n:nat) + (ad_0_path_dist_1 x y (nil ad) n)=(ad_simple_path_dist_1 cg x y (nil ad) n). + Proof. + Intros. Apply Ddle_antisym. Apply ad_0_path_dist_1_le. + Exact (CG_circuits_non_negative_weight cg H). + Apply ad_0_path_dist_1_ge. + Qed. + +Lemma ad_0_path_dist_correct : (CGconsistent cg) -> + (x,y:ad) (ad_0_path_dist x y)=(ad_simple_path_dist cg x y). + Proof. + Intros. Exact (ad_0_path_dist_correct_1 H x y (MapCard ? cg)). + Qed. + +(*s Uses a set [s] of already visited nodes *) + +Fixpoint ad_1_path_dist_1 [x,y:ad; s:FSet; n:nat] : (option D) := + if (ad_eq x y) + then (SOME ? Dz) + else + Cases n of + O => (NONE ?) + | (S n') => Cases (MapGet ? cg x) of + NONE => (NONE ?) + | (SOME edges) => + Cases (MapGet ? s x) of + (SOME _) => (NONE ?) + | NONE => let s'=(MapPut unit s x tt) in + (all_min [z:ad][d:D] + Cases (MapGet ? s' z) of + (SOME _) => (NONE D) + | NONE => (Ddplus (ad_1_path_dist_1 z y s' n') d) + end + edges) + end + end + end. + +Definition ad_1_path_dist := [x,y:ad] + (ad_1_path_dist_1 x y (M0 unit) (MapCard ? cg)). + +Lemma ad_1_path_dist_correct_1 : (n:nat) (x,y:ad) (l:(list ad)) + (ad_1_path_dist_1 x y (Elems l) n)=(ad_0_path_dist_1 x y l n). + Proof. + Induction n. Trivial. + Simpl. Intros. Case (ad_eq x y). Reflexivity. + Case (MapGet ? cg x). Reflexivity. + Intro. Unfold all_min. Elim (sumbool_of_bool (ad_in_list x l)). Intro H0. Rewrite H0. + Rewrite <- (ad_in_elems_in_list l x) in H0. Elim (in_dom_some ? ? ? H0). Intros t H1. + Rewrite H1. Reflexivity. + Intro H0. Rewrite H0. Rewrite <- (ad_in_elems_in_list l x) in H0. + Rewrite (in_dom_none ? ? ? H0). Apply MapFold_ext_f. Intros. + Elim (sumbool_of_bool (ad_in_list a (cons x l))). Intro H2. + Rewrite <- (ad_in_elems_in_list (cons x l) a) in H2. Elim (in_dom_some ? ? ? H2). Simpl. + Intro t. Elim t. Intro H3. Rewrite H3. Rewrite (ad_in_elems_in_list (cons x l) a) in H2. + Simpl in H2. Rewrite H2. Reflexivity. + Intro H2. Cut (orb (ad_eq a x) (ad_in_list a l))=false. Intro H3. Rewrite H3. + Rewrite <- (ad_in_elems_in_list (cons x l) a) in H2. Simpl in H2. + Rewrite (in_dom_none ? ? ? H2). Rewrite <- (H a y (cons x l)). Reflexivity. + Assumption. + Qed. + +Lemma ad_1_path_dist_correct_2 : (x,y:ad) (ad_1_path_dist x y)=(ad_0_path_dist x y). + Proof. + Intros. Exact (ad_1_path_dist_correct_1 (MapCard ? cg) x y (nil ad)). + Qed. + +Lemma ad_1_path_dist_correct_3 : (CGconsistent cg) -> + (n:nat) (x,y:ad) + (ad_1_path_dist_1 x y (M0 unit) n)=(ad_simple_path_dist_1 cg x y (nil ad) n). + Proof. + Intros. Rewrite <- (ad_0_path_dist_correct_1 H x y n). + Exact (ad_1_path_dist_correct_1 n x y (nil ad)). + Qed. + +Lemma ad_1_path_dist_correct : (CGconsistent cg) -> + (x,y:ad) (ad_1_path_dist x y)=(ad_simple_path_dist cg x y). + Proof. + Intros. Rewrite ad_1_path_dist_correct_2. Apply ad_0_path_dist_correct. Assumption. + Qed. + +Lemma ad_1_path_dist_big_enough_1 : (n:nat) (s:FSet) + (MapSubset ? ? s (MapDom ? cg)) -> + (le (MapCard ? cg) (plus n (MapCard ? s))) -> + (x,y:ad) (ad_1_path_dist_1 x y s n)=(ad_1_path_dist_1 x y s (S n)). + Proof. + Induction n. Intros. Simpl. Case (ad_eq x y). Reflexivity. + Elim (sumbool_of_bool (in_dom ? x cg)). Intro H1. Elim (in_dom_some ? ? ? H1). + Intros edges H2. Rewrite H2. Elim (sumbool_of_bool (in_dom ? x s)). Intro H3. + Elim (in_dom_some ? ? ? H3). Intros t H4. Rewrite H4. Reflexivity. + Intro H3. Simpl in H0. Rewrite (MapCard_Dom ? cg) in H0. Rewrite (MapDom_Dom ? s x) in H3. + Cut (MapGet ? (MapDom unit s) x)=(NONE ?). Rewrite (MapSubset_card_eq ? ? ? ? H H0 x). + Rewrite (FSet_Dom (MapDom ? cg)). + Elim (in_dom_some ? ? ? (MapDom_semantics_1 ? cg x edges H2)). Intros t H4 H5. + Rewrite H4 in H5. Discriminate H5. + Exact (in_dom_none ? ? ? H3). + Intro H1. Rewrite (in_dom_none ? ? ? H1). Reflexivity. + Intros. Cut (m:nat) m=(S n0)->(ad_1_path_dist_1 x y s (S n0))=(ad_1_path_dist_1 x y s (S m)). + Intro. Exact (H2 (S n0) (refl_equal ? ?)). + Intros. Simpl. Case (ad_eq x y). Reflexivity. + Elim (option_sum ? (MapGet ? cg x)). Intro H'. Elim H'. Intros edges H'0. Rewrite H'0. + Elim (option_sum ? (MapGet ? s x)). Intro H3. Elim H3. Intros t H4. Rewrite H4. Reflexivity. + Intro H3. Rewrite H3. Unfold all_min. Apply MapFold_ext_f. Intros. + Rewrite (MapPut_semantics unit s x tt a). Elim (sumbool_of_bool (ad_eq x a)). Intro H5. + Rewrite H5. Reflexivity. + Intro H5. Rewrite H5. Case (MapGet ? s a). Rewrite H2. Rewrite H. Reflexivity. + Unfold MapSubset. Intros. Elim (in_dom_some ? ? ? H6). Intro. + Rewrite (MapPut_semantics unit s x tt a0). Elim (sumbool_of_bool (ad_eq x a0)). Intro H7. + Rewrite H7. Intro H8. Rewrite <- (ad_eq_complete ? ? H7). Fold (in_FSet x (MapDom ? cg)). + Rewrite <- (MapDom_Dom ? cg x). Unfold in_dom. Rewrite H'0. Reflexivity. + Intro H7. Rewrite H7. Intro H8. Apply (H0 a0). Unfold in_dom. Rewrite H8. Reflexivity. + Rewrite MapCard_Put_2_conv. Rewrite <- plus_Snm_nSm. Exact H1. + Assumption. + Trivial. + Intro H3. Rewrite H3. Reflexivity. + Qed. + +Lemma ad_1_path_dist_big_enough_2 : (n:nat) + (x,y:ad) (ad_1_path_dist x y)=(ad_1_path_dist_1 x y (M0 unit) (plus n (MapCard ? cg))). + Proof. + Induction n. Trivial. + Intros. Unfold plus. Fold (plus n0 (MapCard ? cg)). Rewrite <- ad_1_path_dist_big_enough_1. + Apply H. + Unfold MapSubset. Intros. Discriminate H0. + Simpl. Rewrite <- plus_n_O. Apply le_plus_r. + Qed. + +Lemma ad_1_path_dist_big_enough : (n:nat) (le (MapCard ? cg) n) -> + (x,y:ad) (ad_1_path_dist x y)=(ad_1_path_dist_1 x y (M0 unit) n). + Proof. + Intros. Cut (EX m:nat | n=(plus m (MapCard ? cg))). Intro H0. Elim H0. Intros m H1. + Rewrite H1. Apply ad_1_path_dist_big_enough_2. + Elim H. Split with O. Reflexivity. + Intros. Elim H1. Intros m' H2. Split with (S m'). Rewrite H2. Reflexivity. + Qed. + +End CGDist1. + +(*s Definition of concrete formulas : + [(CGleq x y d)] means $x\leq y+d$, [(CGeq x y d)] means $x=y+d$ + *) + +Inductive CGForm : Set := + CGleq : ad -> ad -> D -> CGForm + | CGeq : ad -> ad -> D -> CGForm + | CGand : CGForm -> CGForm -> CGForm + | CGor : CGForm -> CGForm -> CGForm + | CGimp : CGForm -> CGForm -> CGForm + | CGnot : CGForm -> CGForm. + +(*s Interpretation of concrete formulas as proposition *) + +Fixpoint CGeval [rho:ad->D; f:CGForm] : Prop := + Cases f of + (CGleq x y d) => (Dle (rho x) (Dplus (rho y) d))=true + | (CGeq x y d) => (rho x)=(Dplus (rho y) d) + | (CGand f0 f1) => (CGeval rho f0) /\ (CGeval rho f1) + | (CGor f0 f1) => (CGeval rho f0) \/ (CGeval rho f1) + | (CGimp f0 f1) => (CGeval rho f0) -> (CGeval rho f1) + | (CGnot f0) => ~(CGeval rho f0) + end. + +(*s Decidability of satisfaction *) + +Lemma CGeval_dec : (f:CGForm) (rho:ad->D) {(CGeval rho f)}+{~(CGeval rho f)}. + Proof. + Induction f. + Intros. Simpl. Elim (sumbool_of_bool (Dle (rho a) (Dplus (rho a0) d))). + Intro H. Left . Assumption. + Intro H. Right . Unfold not. Rewrite H. Intro H0. Discriminate H0. + Simpl. Intros. Apply D_dec. + Simpl. Intros. Elim (H rho). Intro H1. Elim (H0 rho). Intro H2. Left . (Split; Assumption). + Unfold not. Intro H2. Right . Intro. Elim H3. Intro. Assumption. + Unfold not. Intro H1. Right . Intro H2. Elim H2. Intros. Apply (H1 H3). + Simpl. Intros. Elim (H rho). Intro H1. Left . Left . Assumption. + Elim (H0 rho). Intros H1 H2. Left . Right . Assumption. + Unfold not. Intros H1 H2. Right . Intro H3. (Elim H3; Assumption). + Simpl. Intros. Elim (H0 rho). Intro H1. Left . Intro H2. Assumption. + Elim (H rho). Unfold not. Intros H1 H2. Right . Intro H3. Apply H2. Apply H3. Assumption. + Unfold not. Intros H1 H2. Left . Intro H3. Elim (H1 H3). + Intros. Simpl. Elim (H rho). Intro H0. Right . Unfold not. Intros. Exact (H1 H0). + Intro H0. Left . Assumption. + Qed. + +(*s Simplified formulae: *) +Inductive CGSForm : Set := + CGSleq : ad -> ad -> D -> CGSForm + | CGSand : CGSForm -> CGSForm -> CGSForm + | CGSor : CGSForm -> CGSForm -> CGSForm. + +Fixpoint CG_of_CGS [fs:CGSForm] : CGForm := + Cases fs of + (CGSleq x y d) => (CGleq x y d) + | (CGSand fs0 fs1) => (CGand (CG_of_CGS fs0) (CG_of_CGS fs1)) + | (CGSor fs0 fs1) => (CGor (CG_of_CGS fs0) (CG_of_CGS fs1)) + end. + +Definition CGSeval := [rho:ad->D; fs:CGSForm] (CGeval rho (CG_of_CGS fs)). + +(*s Decision procedure for simplified formulae *) + +Section CGSSolve. + + Variable anchor : ad. + Variable anchor_value : D. + +(*s Is $x\leq y+d$ consistent with [cg]? *) + +Definition CG_test_ineq := [cg:CGraph1; n:nat; x,y:ad; d:D] + (Ddle (SOME ? (Dneg d)) (ad_1_path_dist_1 cg y x (M0 unit) n)). + + Variable def_answer : bool. + +(*s Invariants: [cg] is consistent, [|cg|<=n]. + [(CGS_solve_1 cg n fsl gas)] + returns [true] iff [cg /\ fsl /\ anchor=anchor_value] is consistent, + where [fsl] is understood as the conjunction of all the [fs] in [fsl]; + i.e. iff [cg /\ fsl] alone is consistent + (lemmas [CG_anchored_then_consistent] and [CG_consistent_then_anchored)]. + [gas] is intended to be [>=] the sum of sizes of all formulas in [fsl]. *) + +Fixpoint CGS_solve_1 [cg:CGraph1; n:nat; fsl:(list CGSForm); gas:nat] : bool := + Cases gas of + O => def_answer + | (S gas') => + Cases fsl of + nil => true + | (cons fs fsl') => + Cases fs of + (CGSleq x y d) => if (CG_test_ineq cg n x y d) + then let cg' = (CG_add cg x y d) in + (CGS_solve_1 cg' (S n) fsl' gas') + else false + | (CGSand fs0 fs1) => (CGS_solve_1 cg n (cons fs0 (cons fs1 fsl')) gas') + | (CGSor fs0 fs1) => if (CGS_solve_1 cg n (cons fs0 fsl') gas') + then true + else (CGS_solve_1 cg n (cons fs1 fsl') gas') + end + end + end. + +(*s Size of a set of formula and of a list of formula *) + +Fixpoint FSize [f:CGSForm] : nat := + Cases f of + (CGSand f0 f1) => (S (plus (FSize f0) (FSize f1))) + | (CGSor f0 f1) => (S (plus (FSize f0) (FSize f1))) + | _ => (1) + end. + +Fixpoint FlSize [fsl:(list CGSForm)] : nat := + Cases fsl of + nil => O + | (cons fs fsl') => (plus (FSize fs) (FlSize fsl')) + end. + + +Definition CGS_solve := [fs:CGSForm] (CGS_solve_1 (M0 ?) O (cons fs (nil ?)) (S (FSize fs))). + +(*s Interpretation of a list of formula as a conjonction *) + +Fixpoint CGSeval_l [rho:ad->D; fsl:(list CGSForm)] : Prop := + Cases fsl of + nil => True + | (cons fs fsl') => (CGSeval rho fs) /\ (CGSeval_l rho fsl') + end. + +Lemma FSize_geq_1 : (fs:CGSForm) {n:nat | (FSize fs)=(S n)}. + Proof. + Induction fs. Simpl. Intros. Split with O. Reflexivity. + Intros. Simpl. Split with (plus (FSize c) (FSize c0)). Reflexivity. + Intros. Simpl. Split with (plus (FSize c) (FSize c0)). Reflexivity. + Qed. + +Lemma FlSize_is_O : (fsl:(list CGSForm)) (FlSize fsl)=O -> fsl=(nil ?). + Proof. + Induction fsl. Trivial. + Intros. Simpl in H0. Elim (FSize_geq_1 a). Intros n H1. Rewrite H1 in H0. Discriminate H0. + Qed. + +Lemma CG_add_card_le : (cg:CGraph1) (x,y:ad) (d:D) (n:nat) + (le (MapCard ? cg) n) -> (le (MapCard ? (CG_add cg x y d)) (S n)). + Proof. + Intros. Unfold CG_add. Case (MapGet ? cg x). + Apply (le_trans ? ? (S n) (MapCard_Put_ub ? cg x (M1 D y d))). Apply le_n_S. Assumption. + Intro. Case (MapGet ? m y). + Apply (le_trans ? ? (S n) (MapCard_Put_ub ? cg x (MapPut D m y d))). Apply le_n_S. + Assumption. + Intro. Apply (le_trans ? ? (S n) (MapCard_Put_ub ? cg x (MapPut D m y (Dmin d d0)))). + Apply le_n_S. Assumption. + Qed. + +Lemma CGS_solve_1_correct : (gas:nat) (fsl:(list CGSForm)) (cg:CGraph1) (n:nat) + (CGconsistent cg) -> + (le (MapCard ? cg) n) -> + (lt (FlSize fsl) gas) -> + (CGS_solve_1 cg n fsl gas)=true -> + {rho:ad->D | (CGSeval_l rho fsl) /\ (CGsat cg rho)}. + Proof. + Induction gas. Intros. Elim (lt_n_O ? H1). + Simpl. Intros n H fsl. Case fsl. Intros. Elim H0. Intros rho H4. Split with rho. + Split. Exact I. + Assumption. + Intro fs. Case fs. Intros. Elim (sumbool_of_bool (CG_test_ineq cg n0 a a0 d)). Intro H4. + Rewrite H4 in H3. Unfold CG_test_ineq in H4. Elim (H l (CG_add cg a a0 d) (S n0)). + Intros rho H5. Split with rho. Elim H5. Intros. Split. Simpl. Split. Unfold CGSeval. + Simpl. Exact (CG_add_3 cg a a0 d rho H7). + Assumption. + Exact (CG_add_2 cg a a0 d rho H7). + Apply CG_circuit_complete. + Rewrite <- (ad_1_path_dist_big_enough cg n0 H1 a0 a) in H4. + Rewrite (ad_1_path_dist_correct cg H0 a0 a) in H4. + Exact (CG_add_5 cg a a0 d (CG_circuits_non_negative_weight cg H0) H4). + Apply CG_add_card_le. Assumption. + Exact (lt_S_n ? ? H2). + Assumption. + Intro H4. Rewrite H4 in H3. Discriminate H3. + Intros. Elim (H (cons c (cons c0 l)) cg n0 H0). Simpl. Intros rho H4. Split with rho. + Elim H4. Intros. Split; Try Assumption. Elim H5. Intros. Elim H8. Intros. + Split; Try Assumption. Exact (conj ? ? H7 H9). + Assumption. + Simpl. Simpl in H2. Rewrite plus_assoc_l. Apply lt_S_n. Assumption. + Assumption. + Intros. Elim (sumbool_of_bool (CGS_solve_1 cg n0 (cons c l) n)). Intro H4. + Elim (H (cons c l) cg n0 H0 H1). Intros rho H5. Split with rho. Elim H5. Intros. Simpl. + Split; Try Assumption. Split; Try Assumption. Unfold CGSeval. Simpl. Left . Simpl in H6. + Exact (proj1 ? ? H6). + Exact (proj2 ? ? H6). + Simpl. Simpl in H2. Apply le_lt_trans with m:=(plus (plus (FSize c) (FSize c0)) (FlSize l)). + Apply le_reg_r. Apply le_plus_l. + Apply lt_S_n. Assumption. + Assumption. + Intro H4. Rewrite H4 in H3. Elim (H (cons c0 l) cg n0 H0). Intros rho H5. Elim H5. + Intros. Split with rho. Split; Try Assumption. Simpl. Simpl in H6. Elim H6. Intros. + Split; Try Assumption. Unfold CGSeval. Simpl. Right . Assumption. + Assumption. + Simpl. Simpl in H2. Apply le_lt_trans with m:=(plus (plus (FSize c) (FSize c0)) (FlSize l)). + Apply le_reg_r. Apply le_plus_r. + Apply lt_S_n. Assumption. + Assumption. + Qed. + +Lemma CGS_solve_correct : (fs:CGSForm) (CGS_solve fs)=true -> + {rho:ad->D | (CGSeval rho fs)}. + Proof. + Intros. Elim (CGS_solve_1_correct (S (FSize fs)) (cons fs (nil ?)) (M0 ?) O). Intros rho H0. + Simpl in H0. Elim H0. Intros. Elim H1. Intros. Split with rho. Assumption. + Split with [x:ad]Dz. Unfold CGsat. Unfold CG_edge. Simpl. Intros. Discriminate H0. + Apply le_n. + Simpl. Rewrite <- plus_n_O. Unfold lt. Apply le_n. + Exact H. + Qed. + +Lemma CGS_translate_l : (fs:CGSForm) (rho:ad->D) (d:D) (CGSeval rho fs) -> + (CGSeval [a:ad] (Dplus d (rho a)) fs). + Proof. + Induction fs. Unfold CGSeval. Simpl. Intros. Rewrite Dplus_assoc. Apply Dle_plus_mono. + Apply Dle_refl. + Assumption. + Unfold CGSeval. Simpl. Intros. Elim H1. Intros. Split. Apply H. Assumption. + Apply H0. Assumption. + Unfold CGSeval. Simpl. Intros. Elim H1. Intro. Left . Apply H. Assumption. + Intro. Right . Apply H0. Assumption. + Qed. + +Lemma CGS_solve_correct_anchored : (fs:CGSForm) (CGS_solve fs)=true -> + {rho:ad->D | (CGSeval rho fs) /\ (rho anchor)=anchor_value}. + Proof. + Intros. Elim (CGS_solve_correct fs H). Intros rho H0. + Split with [a:ad](Dplus (Dplus anchor_value (Dneg (rho anchor))) (rho a)). Split. + Apply CGS_translate_l. Assumption. + Rewrite Dplus_assoc. Rewrite Dplus_neg_2. Apply Dplus_d_z. + Qed. + +Lemma CGS_solve_complete_1 : (gas:nat) (fsl:(list CGSForm)) (cg:CGraph1) (n:nat) + (lt (FlSize fsl) gas) -> (le (MapCard ? cg) n) -> + (rho:ad->D) (CGsat cg rho) -> (CGSeval_l rho fsl) -> (CGS_solve_1 cg n fsl gas)=true. + Proof. + Induction gas. Intros. Elim (lt_n_O ? H). + Intros n H fsl. Case fsl. Trivial. + Intro fs. Case fs. Simpl. Intros. Unfold CG_test_ineq. + Rewrite <- (ad_1_path_dist_big_enough cg n0 H1 a0 a). Cut (CGconsistent cg). Intro H4. + Rewrite (ad_1_path_dist_correct cg H4 a0 a). Elim H3. Intros. + Rewrite (CG_sat_add_1 cg a a0 d rho H2 H5). Apply H with rho:=rho. Apply lt_S_n. Assumption. + Apply CG_add_card_le. Assumption. + Fold (cg2 cg a a0 d). Apply CG_add_1. Assumption. + Exact H5. + Assumption. + Split with rho. Assumption. + Simpl. Intros. Apply H with rho:=rho. Simpl. Rewrite plus_assoc_l. Apply lt_S_n. Assumption. + Assumption. + Assumption. + Elim H3. Intros. Simpl. Elim H4. Intros. Split; Try Assumption. Split; Assumption. + Simpl. Intros. Elim H3. Intros. Elim H4. Intro. Cut (CGS_solve_1 cg n0 (cons c l) n)=true. + Intro H7. Rewrite H7. Reflexivity. + Apply H with rho:=rho. Simpl. + Apply le_lt_trans with m:=(plus (plus (FSize c) (FSize c0)) (FlSize l)). Apply le_reg_r. + Apply le_plus_l. + Apply lt_S_n. Assumption. + Assumption. + Assumption. + Split; Assumption. + Intro H6. Cut (CGS_solve_1 cg n0 (cons c0 l) n)=true. Intro H7. + Case (CGS_solve_1 cg n0 (cons c l) n); Trivial. + Apply H with rho:=rho. Simpl. + Apply le_lt_trans with m:=(plus (plus (FSize c) (FSize c0)) (FlSize l)). Apply le_reg_r. + Apply le_plus_r. + Apply lt_S_n. Assumption. + Assumption. + Assumption. + Split; Assumption. + Qed. + +Lemma CGS_solve_complete : (fs:CGSForm) (rho:ad->D) + (CGSeval rho fs) -> (CGS_solve fs)=true. + Proof. + Intros. Apply (CGS_solve_complete_1 (S (FSize fs)) (cons fs (nil ?)) (M0 ?) O) with rho:=rho. + Simpl. Rewrite <- plus_n_O. Unfold lt. Apply le_n. + Apply le_n. + Unfold CGsat. Intros. Unfold CG_edge in H0. Discriminate H0. + Simpl. Split; Trivial. + Qed. + +Definition CGSeq := [x,y:ad] [d:D] (CGSand (CGSleq x y d) (CGSleq y x (Dneg d))). + +Lemma CGSeq_correct : (x,y:ad) (d:D) (rho:ad->D) + (CGSeval rho (CGSeq x y d)) -> (rho x)=(Dplus (rho y) d). + Proof. + Intros. Unfold CGSeq CGSeval in H. Simpl in H. Elim H. Intros. Apply Dle_antisym. Assumption. + Apply Dplus_reg_r with d'':=(Dneg d). Rewrite Dplus_assoc. Rewrite Dplus_neg. + Rewrite Dplus_d_z. Assumption. + Qed. + +Lemma CGSeq_complete : (x,y:ad) (d:D) (rho:ad->D) + (rho x)=(Dplus (rho y) d) -> (CGSeval rho (CGSeq x y d)). + Proof. + Intros. Unfold CGSeq CGSeval. Simpl. Rewrite H. Split. Apply Dle_refl. + Rewrite Dplus_assoc. Rewrite Dplus_neg. Rewrite Dplus_d_z. Apply Dle_refl. + Qed. + +End CGSSolve. + +Section CGWithOne. + + Variable Done : D. + Variable Done_pos : (Dle Done Dz)=false. + Variable Done_min_pos : (d:D) (Dle d Dz)=false -> (Dle Done d)=true. + +(*s Defining the negation of a formula : + $\neg x \leq y+d \Leftrightarrow x>y+d \Leftrightarrow x \geq y+d+1$ + *) +Fixpoint CGSnot [fs:CGSForm] : CGSForm := + Cases fs of + (CGSleq x y d) => (CGSleq y x (Dneg (Dplus d Done))) + + | (CGSand f0 f1) => (CGSor (CGSnot f0) (CGSnot f1)) + | (CGSor f0 f1) => (CGSand (CGSnot f0) (CGSnot f1)) + end. + +Lemma Dmone_neg : (Dle Dz (Dneg Done))=false. + Proof. + Elim (sumbool_of_bool (Dle Dz (Dneg Done))). Intro H. + Rewrite <- (Dneg_neg Done) in Done_pos. + Rewrite (Dle_neg ? H) in Done_pos. Discriminate Done_pos. + Trivial. + Qed. + +Lemma Dminus_one_1 : (d:D) (Dle d (Dplus d (Dneg Done)))=false. + Proof. + Intro. Elim (sumbool_of_bool (Dle d (Dplus d (Dneg Done)))). Intro H. + Cut (Dle Dz (Dneg Done))=true. Intro. Rewrite Dmone_neg in H0. Discriminate H0. + Apply Dplus_reg_l with d'':=d. Rewrite Dplus_d_z. Assumption. + Trivial. + Qed. + +Lemma Dle_lt_1 : (d,d':D) (Dle d' d)=false -> (Dle d (Dplus d' (Dneg Done)))=true. + Proof. + Intros. Apply Dplus_reg_r with d'':=Done. Rewrite Dplus_assoc. Rewrite Dplus_neg_2. + Rewrite Dplus_d_z. Apply Dplus_reg_l with d'':=(Dneg d). Rewrite <- Dplus_assoc. + Rewrite Dplus_neg_2. Rewrite Dplus_z_d. Apply Done_min_pos. + Elim (sumbool_of_bool (Dle (Dplus (Dneg d) d') Dz)). Intro H0. Cut (Dle d' d)=true. + Rewrite H. Intro. Discriminate H1. + Apply Dplus_reg_l with d'':=(Dneg d). Rewrite Dplus_neg_2. Assumption. + Trivial. + Qed. + +Lemma Dle_lt_2 : (d,d':D) (Dle d (Dplus d' (Dneg Done)))=true -> (Dle d' d)=false. + Proof. + Intros. Elim (sumbool_of_bool (Dle d' d)). Intro H0. Cut (Dle d (Dplus d (Dneg Done)))=true. + Rewrite Dminus_one_1. Intro. Discriminate H1. + Apply Dle_trans with d':=(Dplus d' (Dneg Done)). Assumption. + Apply Dle_plus_mono. Assumption. + Apply Dle_refl. + Trivial. + Qed. + +Lemma CGSnot_correct : (fs:CGSForm) (rho:ad->D) (CGSeval rho fs) -> ~(CGSeval rho (CGSnot fs)). + Proof. + Unfold not. Induction fs. Simpl. Unfold CGSeval. Simpl. Intros. + Cut (Dle (rho a) (Dplus (rho a) (Dneg Done)))=true. Rewrite Dminus_one_1. Intro. + Discriminate H1. + Rewrite <- (Dplus_d_z (Dneg Done)). Rewrite <- (Dplus_neg_2 d). + Rewrite <- (Dplus_assoc (Dneg Done)). Rewrite <- Dneg_plus. + Apply Dle_trans with d':=(Dplus (rho a0) d). Assumption. + Rewrite <- Dplus_assoc. Apply Dle_plus_mono. Assumption. + Apply Dle_refl. + Unfold CGSeval. Simpl. Intros. Elim H1. Intros. Elim H2. Intro. Exact (H rho H3 H5). + Intro. Exact (H0 rho H4 H5). + Unfold CGSeval. Simpl. Intros. Elim H2. Intros. Elim H1. Intro. Exact (H rho H5 H3). + Intro. Exact (H0 rho H5 H4). + Qed. + +Lemma CGSnot_complete : (fs:CGSForm) (rho:ad->D) + ~(CGSeval rho (CGSnot fs)) -> (CGSeval rho fs). + Proof. + Unfold not CGSeval. Induction fs. Simpl. Intros. + Elim (sumbool_of_bool (Dle (rho a) (Dplus (rho a0) d))). Trivial. + Intro H0. Cut False. Intro. Elim H1. + Apply H. Rewrite Dneg_plus. Rewrite <- Dplus_assoc. Apply Dplus_reg_r with d'':=d. + Rewrite Dplus_assoc. Rewrite Dplus_neg_2. Rewrite Dplus_d_z. Apply Dle_lt_1. Assumption. + Simpl. Intros. Split. Apply H. Intro. Apply H1. Left . Assumption. + Apply H0. Intro. Apply H1. Right . Assumption. + Simpl. Intros. + Cut ~(CGeval rho (CG_of_CGS (CGSnot c))) \/ ~(CGeval rho (CG_of_CGS (CGSnot c0))). Intro. + Elim H2. Intro. Left . Apply H. Assumption. + Intro. Right . Apply H0. Assumption. + Elim (CGeval_dec (CG_of_CGS (CGSnot c)) rho). Intro H2. + Elim (CGeval_dec (CG_of_CGS (CGSnot c0)) rho). Intro H3. Elim (H1 (conj ? ? H2 H3)). + Intro H3. Right . Assumption. + Intro H2. Left . Assumption. + Qed. + +(*s Interpreting formula as simplified formula *) + +Fixpoint CGFormSimplify [f:CGForm] : CGSForm := + Cases f of + (CGleq x y d) => (CGSleq x y d) + | (CGeq x y d) => (CGSeq x y d) + | (CGand f0 f1) => (CGSand (CGFormSimplify f0) (CGFormSimplify f1)) + | (CGor f0 f1) => (CGSor (CGFormSimplify f0) (CGFormSimplify f1)) + | (CGimp f0 f1) => (CGSor (CGSnot (CGFormSimplify f0)) (CGFormSimplify f1)) + | (CGnot f0) => (CGSnot (CGFormSimplify f0)) + end. + +Lemma CGFormSimplify_correct : (f:CGForm) (rho:ad->D) + (CGeval rho f) <-> (CGSeval rho (CGFormSimplify f)). + Proof. + Induction f. Intros. Split; Trivial. + Intros. Unfold CGSeval. Simpl. Split. Intro H. Exact (CGSeq_complete a a0 d rho H). + Exact (CGSeq_correct a a0 d rho). + Simpl. Intros. Unfold CGSeval. Simpl. Elim (H rho). Intros. Elim (H0 rho). Intros. + Split. Intro. Elim H5. Intros. Split. Apply H1. Assumption. + Apply H3. Assumption. + Intro. Elim H5. Intros. Split. Apply H2. Assumption. + Apply H4. Assumption. + Simpl. Intros. Unfold CGSeval. Elim (H rho). Intros. Elim (H0 rho). Intros. Simpl. Split. + Intro. Elim H5. Intro. Left . Apply H1. Assumption. + Intro. Right . Apply H3. Assumption. + Intro. Elim H5. Intro. Left . Apply H2. Assumption. + Intro. Right . Apply H4. Assumption. + Simpl. Intros. Unfold CGSeval. Simpl. Elim (H rho). Intros. Elim (H0 rho). Intros. Split. + Intro. Elim (CGeval_dec c rho). Intro H6. Right . Apply H3. Apply H5. Assumption. + Intro H6. Left . Elim (CGeval_dec (CG_of_CGS (CGSnot (CGFormSimplify c))) rho). Trivial. + Intro H7. Elim (H6 (H2 (CGSnot_complete ? ? H7))). + Intro. Elim H5. Intros. Elim (CGeval_dec (CG_of_CGS (CGFormSimplify c)) rho). Intro H8. + Elim (CGSnot_correct ? ? H8 H6). + Intro H8. Elim (H8 (H1 H7)). + Intros. Apply H4. Assumption. Simpl. Intros. Unfold CGSeval. Simpl. Elim (H rho). Intros. + Split. Intro. Elim (CGeval_dec (CG_of_CGS (CGSnot (CGFormSimplify c))) rho). Trivial. + Intro H3. Elim (H2 (H1 (CGSnot_complete ? ? H3))). + Unfold not. Intros. Elim (CGSnot_correct ? ? (H0 H3) H2). + Qed. + +(*s Formula are solved by looking at their simplified form *) + +Definition CG_solve := [f:CGForm] (CGS_solve false (CGFormSimplify f)). + +Theorem CG_solve_correct : (f:CGForm) (CG_solve f)=true -> {rho:ad->D | (CGeval rho f)}. + Proof. + Intros. Elim (CGS_solve_correct ? ? H). Intros rho H0. Split with rho. + Apply (proj2 ? ? (CGFormSimplify_correct f rho)). Assumption. + Qed. + +Theorem CG_solve_correct_anchored : (anchor:ad) (anchor_value:D) + (f:CGForm) (CG_solve f)=true -> + {rho:ad->D | (CGeval rho f) /\ (rho anchor)=anchor_value}. + Proof. + Intros. Elim (CGS_solve_correct_anchored anchor anchor_value ? ? H). Intros rho H0. + Split with rho. Elim H0. Intros. Split. Apply (proj2 ? ? (CGFormSimplify_correct f rho)). + Assumption. + Assumption. + Qed. + +Theorem CG_solve_complete : (f:CGForm) (rho:ad->D) + (CGeval rho f) -> (CG_solve f)=true. + Proof. + Intros. Unfold CG_solve. Apply (CGS_solve_complete false) with rho:=rho. + Apply (proj1 ? ? (CGFormSimplify_correct f rho)). Assumption. + Qed. + +(*s A formula is proved when its negation cannot be satisfied *) + +Definition CG_prove := [f:CGForm] (negb (CG_solve (CGnot f))). + +Theorem CG_prove_correct : (f:CGForm) (CG_prove f)=true -> (rho:ad->D) (CGeval rho f). + Proof. + Unfold CG_prove CG_solve. Simpl. Intros. Apply (proj2 ? ? (CGFormSimplify_correct f rho)). + Apply CGSnot_complete. Unfold not. Intro. Rewrite (CGS_solve_complete false ? ? H0) in H. + Discriminate H. + Qed. + +Theorem CG_prove_complete : (f:CGForm) ((rho:ad->D) (CGeval rho f)) -> (CG_prove f)=true. + Proof. + Unfold CG_prove CG_solve. Simpl. Intros. + Elim (sumbool_of_bool (CGS_solve false (CGSnot (CGFormSimplify f)))). Intro H0. + Elim (CGS_solve_correct false ? H0). Intros rho H1. + Elim (CGSnot_correct ? ? (proj1 ? ? (CGFormSimplify_correct ? ?) (H rho)) H1). + Intro H0. Rewrite H0. Reflexivity. + Qed. + +Theorem CG_prove_complete_anchored : (f:CGForm) (anchor:ad) (anchor_value:D) + ((rho:ad->D) (rho anchor)=anchor_value -> (CGeval rho f)) -> (CG_prove f)=true. + Proof. + Unfold CG_prove CG_solve. Simpl. Intros. + Elim (sumbool_of_bool (CGS_solve false (CGSnot (CGFormSimplify f)))). Intro H0. + Elim (CGS_solve_correct_anchored anchor anchor_value false ? H0). Intros rho H1. + Elim H1. Intros. + Elim (CGSnot_correct ? ? (proj1 ? ? (CGFormSimplify_correct f rho) (H rho H3)) H2). + Intro H0. Rewrite H0. Reflexivity. + Qed. + + End CGWithOne. + +End ConstraintGraphs. diff --git a/contrib/graphs/zcgraph.v b/contrib/graphs/zcgraph.v new file mode 100644 index 000000000..64d1f9555 --- /dev/null +++ b/contrib/graphs/zcgraph.v @@ -0,0 +1,417 @@ + +(*s The decision procedure is instantiated for Z *) + +Require cgraph. +Require ZArith. +Require Addr. +Require Addec. + +Inductive ZCGForm : Set := + ZCGle : ad -> ad -> ZCGForm (* x<=y *) + | ZCGge : ad -> ad -> ZCGForm (* x>=y *) + | ZCGlt : ad -> ad -> ZCGForm (* x<y *) + | ZCGgt : ad -> ad -> ZCGForm (* x>y *) + | ZCGlep : ad -> ad -> Z -> ZCGForm (* x<=y+k *) + | ZCGgep : ad -> ad -> Z -> ZCGForm (* x>=y+k *) + | ZCGltp : ad -> ad -> Z -> ZCGForm (* x<y+k *) + | ZCGgtp : ad -> ad -> Z -> ZCGForm (* x>y+k *) + | ZCGlem : ad -> ad -> Z -> ZCGForm (* x+k<=y *) + | ZCGgem : ad -> ad -> Z -> ZCGForm (* x+k>=y *) + | ZCGltm : ad -> ad -> Z -> ZCGForm (* x+k<y *) + | ZCGgtm : ad -> ad -> Z -> ZCGForm (* x+k>y *) + | ZCGlepm : ad -> ad -> Z -> Z -> ZCGForm (* x+k<=y+k' *) + | ZCGgepm : ad -> ad -> Z -> Z -> ZCGForm (* x+k>=y+k' *) + | ZCGltpm : ad -> ad -> Z -> Z -> ZCGForm (* x+k<y+k' *) + | ZCGgtpm : ad -> ad -> Z -> Z -> ZCGForm (* x+k>y+k' *) + | ZCGeq : ad -> ad -> ZCGForm (* x=y *) + | ZCGeqp : ad -> ad -> Z -> ZCGForm (* x=y+k *) + | ZCGeqm : ad -> ad -> Z -> ZCGForm (* x+k=y *) + | ZCGeqpm : ad -> ad -> Z -> Z -> ZCGForm (* x+k=y+k' *) + | ZCGzylem : ad -> Z -> ZCGForm (* k<=y *) + | ZCGzygem : ad -> Z -> ZCGForm (* k>=y *) + | ZCGzyltm : ad -> Z -> ZCGForm (* k<y *) + | ZCGzygtm : ad -> Z -> ZCGForm (* k>y *) + | ZCGzylepm : ad -> Z -> Z -> ZCGForm (* k<=y+k' *) + | ZCGzygepm : ad -> Z -> Z -> ZCGForm (* k>=y+k' *) + | ZCGzyltpm : ad -> Z -> Z -> ZCGForm (* k<y+k' *) + | ZCGzygtpm : ad -> Z -> Z -> ZCGForm (* k>y+k' *) + | ZCGzyeqm : ad -> Z -> ZCGForm (* k=y *) + | ZCGzyeqpm : ad -> Z -> Z -> ZCGForm (* k=y+k' *) + | ZCGxzlep : ad -> Z -> ZCGForm (* x<=k *) + | ZCGxzgep : ad -> Z -> ZCGForm (* x>=k *) + | ZCGxzltp : ad -> Z -> ZCGForm (* x<k *) + | ZCGxzgtp : ad -> Z -> ZCGForm (* x>k *) + | ZCGxzlepm : ad -> Z -> Z -> ZCGForm (* x+k<=k' *) + | ZCGxzgepm : ad -> Z -> Z -> ZCGForm (* x+k>=k' *) + | ZCGxzltpm : ad -> Z -> Z -> ZCGForm (* x+k<k' *) + | ZCGxzgtpm : ad -> Z -> Z -> ZCGForm (* x+k>k' *) + | ZCGxzeqp : ad -> Z -> ZCGForm (* x=k *) + | ZCGxzeqpm : ad -> Z -> Z -> ZCGForm (* x+k=k' *) + | ZCGzzlep : Z -> Z -> ZCGForm (* k<=k' *) + | ZCGzzltp : Z -> Z -> ZCGForm (* k<k' *) + | ZCGzzgep : Z -> Z -> ZCGForm (* k>=k' *) + | ZCGzzgtp : Z -> Z -> ZCGForm (* k>k' *) + | ZCGzzeq : Z -> Z -> ZCGForm (* k=k' *) + | ZCGand : ZCGForm -> ZCGForm -> ZCGForm + | ZCGor : ZCGForm -> ZCGForm -> ZCGForm + | ZCGimp : ZCGForm -> ZCGForm -> ZCGForm + | ZCGnot : ZCGForm -> ZCGForm + | ZCGiff : ZCGForm -> ZCGForm -> ZCGForm. + +Definition ZCG_eval := (CGeval Z Zplus Zle_bool). + +(*s Translation of formula on Z into a constraint graph formula. + we reserve [ad_z] as the "zero" variable, + i.e., the one that is anchored at the value `0`. *) + +Fixpoint ZCGtranslate [f:ZCGForm] : (CGForm Z) := + Cases f of + (ZCGle x y) => (CGleq Z x y `0`) + | (ZCGge x y) => (CGleq Z y x `0`) + | (ZCGlt x y) => (CGleq Z x y `-1`) + | (ZCGgt x y) => (CGleq Z y x `-1`) + | (ZCGlep x y k) => (CGleq Z x y k) + | (ZCGgep x y k) => (CGleq Z y x (Zopp k)) + | (ZCGltp x y k) => (CGleq Z x y `k-1`) + | (ZCGgtp x y k) => (CGleq Z y x (Zopp `k+1`)) + | (ZCGlem x y k) => (CGleq Z x y (Zopp k)) + | (ZCGgem x y k) => (CGleq Z y x k) + | (ZCGltm x y k) => (CGleq Z x y (Zopp `k+1`)) + | (ZCGgtm x y k) => (CGleq Z y x `k-1`) + | (ZCGlepm x y k k') => (CGleq Z x y `k'-k`) + | (ZCGgepm x y k k') => (CGleq Z y x `k-k'`) + | (ZCGltpm x y k k') => (CGleq Z x y `k'-k-1`) + | (ZCGgtpm x y k k') => (CGleq Z y x `k-k'-1`) + | (ZCGeq x y) => (CGeq Z x y `0`) + | (ZCGeqp x y k) => (CGeq Z x y k) + | (ZCGeqm x y k) => (CGeq Z y x k) + | (ZCGeqpm x y k k') => (CGeq Z x y `k'-k`) + | (ZCGzylem y k) => (CGleq Z ad_z y (Zopp k)) + | (ZCGzygem y k) => (CGleq Z y ad_z k) + | (ZCGzyltm y k) => (CGleq Z ad_z y (Zopp `k+1`)) + | (ZCGzygtm y k) => (CGleq Z y ad_z `k-1`) + | (ZCGzylepm y k k') => (CGleq Z ad_z y `k'-k`) + | (ZCGzygepm y k k') => (CGleq Z y ad_z `k-k'`) + | (ZCGzyltpm y k k') => (CGleq Z ad_z y `k'-k-1`) + | (ZCGzygtpm y k k') => (CGleq Z y ad_z `k-k'-1`) + | (ZCGzyeqm y k) => (CGeq Z y ad_z k) + | (ZCGzyeqpm y k k') => (CGeq Z y ad_z `k-k'`) + | (ZCGxzlep x k) => (CGleq Z x ad_z k) + | (ZCGxzgep x k) => (CGleq Z ad_z x (Zopp k)) + | (ZCGxzltp x k) => (CGleq Z x ad_z `k-1`) + | (ZCGxzgtp x k) => (CGleq Z ad_z x (Zopp `k+1`)) + | (ZCGxzlepm x k k') => (CGleq Z x ad_z `k'-k`) + | (ZCGxzgepm x k k') => (CGleq Z ad_z x `k-k'`) + | (ZCGxzltpm x k k') => (CGleq Z x ad_z `k'-k-1`) + | (ZCGxzgtpm x k k') => (CGleq Z ad_z x `k-k'-1`) + | (ZCGxzeqp x k) => (CGeq Z x ad_z k) + | (ZCGxzeqpm x k k') => (CGeq Z x ad_z `k'-k`) + | (ZCGzzlep k k') => (CGleq Z ad_z ad_z `k'-k`) + | (ZCGzzltp k k') => (CGleq Z ad_z ad_z `k'-k-1`) + | (ZCGzzgep k k') => (CGleq Z ad_z ad_z `k-k'`) + | (ZCGzzgtp k k') => (CGleq Z ad_z ad_z `k-k'-1`) + | (ZCGzzeq k k') => (CGeq Z ad_z ad_z `k-k'`) + | (ZCGand f0 f1) => (CGand Z (ZCGtranslate f0) (ZCGtranslate f1)) + | (ZCGor f0 f1) => (CGor Z (ZCGtranslate f0) (ZCGtranslate f1)) + | (ZCGimp f0 f1) => (CGimp Z (ZCGtranslate f0) (ZCGtranslate f1)) + | (ZCGnot f0) => (CGnot Z (ZCGtranslate f0)) + | (ZCGiff f0 f1) => (CGand Z (CGimp Z (ZCGtranslate f0) (ZCGtranslate f1)) + (CGimp Z (ZCGtranslate f1) (ZCGtranslate f0))) + end. + +Section ZCGevalDef. + + Variable rho : ad -> Z. + +Fixpoint ZCGeval [f:ZCGForm] : Prop := + Cases f of + (ZCGle x y) => `(rho x)<=(rho y)` + | (ZCGge x y) => `(rho x)>=(rho y)` + | (ZCGlt x y) => `(rho x)<(rho y)` + | (ZCGgt x y) => `(rho x)>(rho y)` + | (ZCGlep x y k) => `(rho x)<=(rho y)+k` + | (ZCGgep x y k) => `(rho x)>=(rho y)+k` + | (ZCGltp x y k) => `(rho x)<(rho y)+k` + | (ZCGgtp x y k) => `(rho x)>(rho y)+k` + | (ZCGlem x y k) => `(rho x)+k<=(rho y)` + | (ZCGgem x y k) => `(rho x)+k>=(rho y)` + | (ZCGltm x y k) => `(rho x)+k<(rho y)` + | (ZCGgtm x y k) => `(rho x)+k>(rho y)` + | (ZCGlepm x y k k') => `(rho x)+k<=(rho y)+k'` + | (ZCGgepm x y k k') => `(rho x)+k>=(rho y)+k'` + | (ZCGltpm x y k k') => `(rho x)+k<(rho y)+k'` + | (ZCGgtpm x y k k') => `(rho x)+k>(rho y)+k'` + | (ZCGeq x y) => `(rho x)=(rho y)` + | (ZCGeqp x y k) => `(rho x)=(rho y)+k` + | (ZCGeqm x y k) => `(rho x)+k=(rho y)` + | (ZCGeqpm x y k k') => `(rho x)+k=(rho y)+k'` + | (ZCGzylem y k) => `k<=(rho y)` + | (ZCGzygem y k) => `k>=(rho y)` + | (ZCGzyltm y k) => `k<(rho y)` + | (ZCGzygtm y k) => `k>(rho y)` + | (ZCGzylepm y k k') => `k<=(rho y)+k'` + | (ZCGzygepm y k k') => `k>=(rho y)+k'` + | (ZCGzyltpm y k k') => `k<(rho y)+k'` + | (ZCGzygtpm y k k') => `k>(rho y)+k'` + | (ZCGzyeqm y k) => `k=(rho y)` + | (ZCGzyeqpm y k k') => `k=(rho y)+k'` + | (ZCGxzlep x k) => `(rho x)<=k` + | (ZCGxzgep x k) => `(rho x)>=k` + | (ZCGxzltp x k) => `(rho x)<k` + | (ZCGxzgtp x k) => `(rho x)>k` + | (ZCGxzlepm x k k') => `(rho x)+k<=k'` + | (ZCGxzgepm x k k') => `(rho x)+k>=k'` + | (ZCGxzltpm x k k') => `(rho x)+k<k'` + | (ZCGxzgtpm x k k') => `(rho x)+k>k'` + | (ZCGxzeqp x k) => `(rho x)=k` + | (ZCGxzeqpm x k k') => `(rho x)+k=k'` + | (ZCGzzlep k k') => `k<=k'` + | (ZCGzzltp k k') => `k<k'` + | (ZCGzzgep k k') => `k>=k'` + | (ZCGzzgtp k k') => `k>k'` + | (ZCGzzeq k k') => `k=k'` + | (ZCGand f0 f1) => (ZCGeval f0) /\ (ZCGeval f1) + | (ZCGor f0 f1) => (ZCGeval f0) \/ (ZCGeval f1) + | (ZCGimp f0 f1) => (ZCGeval f0) -> (ZCGeval f1) + | (ZCGnot f0) => ~(ZCGeval f0) + | (ZCGiff f0 f1) => (ZCGeval f0) <-> (ZCGeval f1) + end. + + Variable Zrho_zero : (rho ad_z)=ZERO. + +Lemma ZCGeval_correct + : (f:ZCGForm) (ZCGeval f) <-> (ZCG_eval rho (ZCGtranslate f)). + Proof. + Induction f; Simpl. Intros. Rewrite Zero_right. Apply Zle_is_le_bool. + Intros. Rewrite Zero_right. Apply Zge_is_le_bool. + Intros. Exact (Zlt_is_le_bool (rho a) (rho a0)). + Intros. Exact (Zgt_is_le_bool (rho a) (rho a0)). + Intros. Apply Zle_is_le_bool. + Intros. Apply iff_trans with b:=`(rho a0)+z <= (rho a)`. Apply Zge_iff_le. + Apply iff_trans with b:=`(rho a0) <= (rho a)-z`. Apply Zle_plus_swap. + Unfold Zminus. Apply Zle_is_le_bool. + Intros. Apply iff_trans with b:=(Zle_bool (rho a) `(rho a0)+z-1`)=true. Apply Zlt_is_le_bool. + Unfold 1 Zminus. Rewrite Zplus_assoc_r. Split; Intro; Assumption. + Intros. Apply iff_trans with b:=`(rho a0)+z < (rho a)`. Apply Zgt_iff_lt. + Apply iff_trans with `(rho a0) < (rho a)-z`. Apply Zlt_plus_swap. + Rewrite Zopp_Zplus. Rewrite Zplus_assoc_l. Exact (Zlt_is_le_bool (rho a0) `(rho a)-z`). + Intros. Apply iff_trans with b:=`(rho a) <= (rho a0)-z`. Apply Zle_plus_swap. + Unfold Zminus. Apply Zle_is_le_bool. + Intros. Apply Zge_is_le_bool. + Intros. Apply iff_trans with b:=`(rho a) < (rho a0)-z`. Apply Zlt_plus_swap. + Rewrite Zopp_Zplus. Rewrite Zplus_assoc_l. Exact (Zlt_is_le_bool (rho a) `(rho a0)-z`). + Intros. Unfold Zminus. Rewrite Zplus_assoc_l. Exact (Zgt_is_le_bool `(rho a)+z` (rho a0)). + Intros. Apply iff_trans with b:=`(rho a) <= (rho a0)+z0-z`. Apply Zle_plus_swap. + Unfold 1 Zminus. Rewrite Zplus_assoc_r. Unfold Zminus. Apply Zle_is_le_bool. + Intros. Apply iff_trans with b:=`(rho a0)+z0 <= (rho a)+z`. Apply Zge_iff_le. + Apply iff_trans with b:=`(rho a0) <= (rho a)+z-z0`. Apply Zle_plus_swap. + Unfold 1 Zminus. Rewrite Zplus_assoc_r. Unfold Zminus. Apply Zle_is_le_bool. + Intros. Apply iff_trans with b:=`(rho a) < (rho a0)+z0-z`. Apply Zlt_plus_swap. + Unfold 2 Zminus. Rewrite Zplus_assoc_l. Unfold 1 Zminus. Rewrite Zplus_assoc_r. + Exact (Zlt_is_le_bool (rho a) `(rho a0)+(z0+ -z)`). + Intros. Apply iff_trans with b:=`(rho a0)+z0 < (rho a)+z`. Apply Zgt_iff_lt. + Apply iff_trans with b:=`(rho a0) < (rho a)+z-z0`. Apply Zlt_plus_swap. + Unfold 2 Zminus. Rewrite Zplus_assoc_l. Unfold 1 Zminus. Rewrite Zplus_assoc_r. + Exact (Zlt_is_le_bool (rho a0) `(rho a)+(z+ -z0)`). + Intros. Rewrite Zero_right. Split; Intro; Assumption. + Split; Intro; Assumption. + Split; Intro; Apply sym_eq; Assumption. + Intros. Unfold Zminus. Rewrite Zplus_assoc_l. Exact (Zeq_plus_swap (rho a) `(rho a0)+z0` z). + Rewrite Zrho_zero. Intros. Apply iff_trans with b:=`0+z <= (rho a)`. Rewrite Zero_left. + Split; Intro; Assumption. + Apply iff_trans with b:=`0 <= (rho a)-z`. Apply Zle_plus_swap. + Unfold Zminus. Apply Zle_is_le_bool. + Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply Zge_is_le_bool. + Rewrite Zrho_zero. Intros. Apply iff_trans with b:=`0+z < (rho a)`. Rewrite Zero_left. + Split; Intro; Assumption. + Apply iff_trans with b:=`0 < (rho a)-z`. Apply Zlt_plus_swap. + Rewrite Zopp_Zplus. Rewrite Zplus_assoc_l. Exact (Zlt_is_le_bool `0` `(rho a)-z`). + Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply Zgt_is_le_bool. + Rewrite Zrho_zero. Intros. Apply iff_trans with b:=`0+z <= (rho a)+z0`. Rewrite Zero_left. + Split; Intro; Assumption. + Apply iff_trans with b:=`0 <= (rho a)+z0-z`. Apply Zle_plus_swap. + Unfold 2 Zminus. Rewrite Zplus_assoc_l. Exact (Zle_is_le_bool `0` `(rho a)+z0-z`). + Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply iff_trans with b:=`(rho a)+z0 <= z`. + Apply Zge_iff_le. + Apply iff_trans with b:=`(rho a) <= z-z0`. Apply Zle_plus_swap. + Apply Zle_is_le_bool. + Rewrite Zrho_zero. Intros. Apply iff_trans with `0+z < (rho a)+z0`. Rewrite Zero_left. + Split; Intro; Assumption. + Apply iff_trans with b:=`0 < (rho a)+z0-z`. Apply Zlt_plus_swap. + Unfold 2 Zminus. Rewrite Zplus_assoc_l. Unfold Zminus. Rewrite Zplus_assoc_l. + Exact (Zlt_is_le_bool `0` `(rho a)+z0+ -z`). + Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply iff_trans with b:=`(rho a)+z0 < z`. + Apply Zgt_iff_lt. + Apply iff_trans with b:=`(rho a) < z-z0`. Apply Zlt_plus_swap. + Apply Zlt_is_le_bool. + Rewrite Zrho_zero. Intros. Rewrite Zero_left. Split; Intro; Apply sym_eq; Assumption. + Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply iff_trans with `(rho a)+z0 = z`. + Split; Intro; Apply sym_eq; Assumption. + Apply Zeq_plus_swap. + Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply Zle_is_le_bool. + Rewrite Zrho_zero. Intros. Apply iff_trans with b:=`0+z <= (rho a)`. Rewrite Zero_left. + Apply Zge_iff_le. + Apply iff_trans with b:=`0 <= (rho a)-z`. Apply Zle_plus_swap. + Exact (Zle_is_le_bool `0` `(rho a)-z`). + Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply Zlt_is_le_bool. + Rewrite Zrho_zero. Intros. Apply iff_trans with b:=`0+z < (rho a)`. Rewrite Zero_left. + Apply Zgt_iff_lt. + Apply iff_trans with b:=`0 < (rho a)-z`. Apply Zlt_plus_swap. + Rewrite Zopp_Zplus. Rewrite Zplus_assoc_l. Exact (Zlt_is_le_bool `0` `(rho a)-z`). + Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply iff_trans with b:=`(rho a) <= z0-z`. + Apply Zle_plus_swap. + Apply Zle_is_le_bool. + Rewrite Zrho_zero. Intros. Apply iff_trans with b:=`0+z0 <= (rho a)+z`. Rewrite Zero_left. + Apply Zge_iff_le. + Apply iff_trans with b:=`0 <= (rho a)+z-z0`. Apply Zle_plus_swap. + Unfold 2 Zminus. Rewrite Zplus_assoc_l. Exact (Zle_is_le_bool `0` `(rho a)+z-z0`). + Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply iff_trans with b:=`(rho a) < z0-z`. + Apply Zlt_plus_swap. + Apply Zlt_is_le_bool. + Rewrite Zrho_zero. Intros. Apply iff_trans with b:=`0+z0 < (rho a)+z`. Rewrite Zero_left. + Apply Zgt_iff_lt. + Apply iff_trans with b:=`0 < (rho a)+z-z0`. Apply Zlt_plus_swap. + Unfold 2 Zminus. Rewrite Zplus_assoc_l. Unfold Zminus. Rewrite Zplus_assoc_l. + Exact (Zlt_is_le_bool `0` `(rho a)+z+ -z0`). + Rewrite Zrho_zero. Intros. Rewrite Zero_left. Split; Intro; Assumption. + Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply Zeq_plus_swap. + Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply iff_trans with b:=`0+z <= z0`. + Rewrite Zero_left. Split; Intro; Assumption. + Apply iff_trans with b:=`0 <= z0-z`. Apply Zle_plus_swap. + Apply Zle_is_le_bool. + Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply iff_trans with b:=`0+z < z0`. + Rewrite Zero_left. Split; Intro; Assumption. + Apply iff_trans with b:=`0 < z0-z`. Apply Zlt_plus_swap. + Apply Zlt_is_le_bool. + Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply iff_trans with b:=`0+z0 <= z`. + Rewrite Zero_left. Apply Zge_iff_le. + Apply iff_trans with b:=`0 <= z-z0`. Apply Zle_plus_swap. + Apply Zle_is_le_bool. + Rewrite Zrho_zero. Intros. Rewrite Zero_left. Apply iff_trans with b:=`0+z0 < z`. + Rewrite Zero_left. Apply Zgt_iff_lt. + Apply iff_trans with b:=`0 < z-z0`. Apply Zlt_plus_swap. + Apply Zlt_is_le_bool. + Rewrite Zrho_zero. Intros. Rewrite Zero_left. Split. Intro. Rewrite H. Apply Zminus_n_n. + Intro. Rewrite <- (Zero_left z0). Rewrite H. Unfold Zminus. Rewrite Zplus_assoc_r. + Rewrite Zplus_inverse_l. Rewrite Zero_right. Reflexivity. + Intros. Elim H. Intros. Elim H0. Intros. Split. Intro. Elim H5. Intros. Split. Apply H1. + Assumption. + Apply H3. Assumption. + Intro. Elim H5. Intros. Split. Apply H2. Assumption. + Apply H4. Assumption. + Intros. Elim H. Intros. Elim H0. Intros. Split. Intro. Elim H5. Intro. Left . Apply H1. + Assumption. + Intro. Right . Apply H3. Assumption. + Intro. Elim H5. Intro. Left . Apply H2. Assumption. + Intro. Right . Apply H4. Assumption. + Intros. Elim H. Intros. Elim H0. Intros. Split. Intros. Apply H3. Apply H5. Apply H2. + Assumption. + Intros. Apply H4. Apply H5. Apply H1. Assumption. + Unfold not. Intros. Elim H. Intros. Split. Intros. Apply H2. Apply H1. Assumption. + Intros. Apply H2. Apply H0. Assumption. + Intros. Fold (ZCG_eval rho (ZCGtranslate z))<->(ZCG_eval rho (ZCGtranslate z0)). Split. + Intro. Apply iff_trans with b:=(ZCGeval z). Apply iff_sym. Assumption. + Apply iff_trans with b:=(ZCGeval z0). Assumption. + Assumption. + Intro. Apply iff_trans with b:=(ZCG_eval rho (ZCGtranslate z)). Assumption. + Apply iff_trans with b:=(ZCG_eval rho (ZCGtranslate z0)). Assumption. + Apply iff_sym. Assumption. + Qed. + +End ZCGevalDef. + +Definition ZCG_solve + := [f:ZCGForm] (CG_solve Z ZERO Zplus Zopp Zle_bool `1` (ZCGtranslate f)). + +Theorem ZCG_solve_correct : + (f:ZCGForm) (ZCG_solve f)=true -> + {rho:ad->Z | (ZCGeval rho f) /\ (rho ad_z)=`0`}. +Proof. + Intros. + Elim (CG_solve_correct_anchored Z ZERO Zplus Zopp Zle_bool Zero_right + Zero_left Zplus_assoc_r Zplus_inverse_r Zle_bool_refl + Zle_bool_antisym Zle_bool_trans Zle_bool_total + Zle_bool_plus_mono `1` Zone_pos Zone_min_pos ad_z `0` ? H). + Intros rho H0. Split with rho. Elim H0. Intros. Split. + Apply (proj2 ? ? (ZCGeval_correct rho H2 f)). Assumption. + Assumption. +Qed. + +Theorem ZCG_solve_complete + : (f:ZCGForm) (rho:ad->Z) + (ZCGeval rho f) -> (rho ad_z)=`0` -> (ZCG_solve f)=true. +Proof. + Intros. Unfold ZCG_solve. + Apply (CG_solve_complete Z ZERO Zplus Zopp Zle_bool Zero_right + Zero_left Zplus_assoc_r Zplus_inverse_r Zle_bool_refl + Zle_bool_antisym Zle_bool_trans Zle_bool_total + Zle_bool_plus_mono `1` Zone_pos Zone_min_pos (ZCGtranslate f) + rho). + Apply (proj1 ? ? (ZCGeval_correct rho H0 f)). Assumption. +Qed. + +Definition ZCG_prove + := [f:ZCGForm] (CG_prove Z ZERO Zplus Zopp Zle_bool `1` (ZCGtranslate f)). + +Theorem ZCG_prove_correct + : (f:ZCGForm) (ZCG_prove f)=true -> + (rho:ad->Z) (rho ad_z)=`0` -> (ZCGeval rho f). +Proof. + Intros. Apply (proj2 ? ? (ZCGeval_correct rho H0 f)). + Exact (CG_prove_correct Z ZERO Zplus Zopp Zle_bool Zero_right Zero_left + Zplus_assoc_r Zplus_inverse_r Zle_bool_refl Zle_bool_antisym + Zle_bool_trans Zle_bool_total Zle_bool_plus_mono `1` Zone_pos + Zone_min_pos ? H rho). +Qed. + +Theorem ZCG_prove_complete + : (f:ZCGForm) + ((rho:ad->Z) (rho ad_z)=`0` -> (ZCGeval rho f)) -> (ZCG_prove f)=true. +Proof. + Intros. Unfold ZCG_prove. + Apply (CG_prove_complete_anchored Z ZERO Zplus Zopp Zle_bool Zero_right + Zero_left Zplus_assoc_r Zplus_inverse_r Zle_bool_refl + Zle_bool_antisym Zle_bool_trans Zle_bool_total + Zle_bool_plus_mono `1` Zone_pos Zone_min_pos (ZCGtranslate f) + ad_z `0`). + Intros. Exact (proj1 ? ? (ZCGeval_correct rho H0 f) (H rho H0)). +Qed. + +(*i Tests: + + Definition v := [n:Z] Cases n of + (POS p) => (ad_x p) + | _ => ad_z + end. + + Lemma test1 : (x,y:Z) `x<=y` -> `x<=y+1`. + Proof. + Intros. + Cut (rho:ad->Z) (rho ad_z)=`0` -> + (ZCGeval rho (ZCGimp (ZCGle (v`1`) (v`2`)) (ZCGlep (v`1`) (v`2`) `1`))). + Intro. + Exact (H0 [a:ad]Case (ad_eq a (v`1`)) of x + Case (ad_eq a (v`2`)) of y + `0` end end + (refl_equal ? ?) + H). + + Intros. Apply ZCG_prove_correct. Compute. Reflexivity. + Assumption. + Qed. + + Lemma test2 : (x,y:Z) ~(`x<=y` -> `x<=y-1`). + Proof. + Intros. + Cut (rho:ad->Z) (rho ad_z)=`0` -> + (ZCGeval rho (ZCGnot (ZCGimp (ZCGle (v `1`) (v `2`)) (ZCGlep (v `1`) (v `2`) `-1`)))). + Intro. + Exact (H [a:ad] Case (ad_eq a (v `1`)) of x + Case (ad_eq a (v `2`)) of y + `0` end end (refl_equal ? ?)). + Intros. Apply ZCG_prove_correct. Compute. (* fails: remains to prove false=true; indeed, + test2 is not provable. *) + <Your Tactic Text here> + <Your Tactic Text here> + +i*) |