(* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require BuiltIn. Require int.Int. (* Why3 assumption *) Definition unit := unit. (* Why3 assumption *) Inductive ref (a:Type) {a_WT:WhyType a} := | mk_ref : a -> ref a. Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a). Existing Instance ref_WhyType. Implicit Arguments mk_ref [[a] [a_WT]]. (* Why3 assumption *) Definition contents {a:Type} {a_WT:WhyType a}(v:(ref a)): a := match v with | (mk_ref x) => x end. Axiom set : forall (a:Type) {a_WT:WhyType a}, Type. Parameter set_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (set a). Existing Instance set_WhyType. Parameter mem: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> Prop. (* Why3 assumption *) Definition infix_eqeq {a:Type} {a_WT:WhyType a}(s1:(set a)) (s2:(set a)): Prop := forall (x:a), (mem x s1) <-> (mem x s2). Axiom extensionality : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a)) (s2:(set a)), (infix_eqeq s1 s2) -> (s1 = s2). (* Why3 assumption *) Definition subset {a:Type} {a_WT:WhyType a}(s1:(set a)) (s2:(set a)): Prop := forall (x:a), (mem x s1) -> (mem x s2). Axiom subset_refl : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)), (subset s s). Axiom subset_trans : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a)) (s2:(set a)) (s3:(set a)), (subset s1 s2) -> ((subset s2 s3) -> (subset s1 s3)). Parameter empty: forall {a:Type} {a_WT:WhyType a}, (set a). (* Why3 assumption *) Definition is_empty {a:Type} {a_WT:WhyType a}(s:(set a)): Prop := forall (x:a), ~ (mem x s). Axiom empty_def1 : forall {a:Type} {a_WT:WhyType a}, (is_empty (empty :(set a))). Axiom mem_empty : forall {a:Type} {a_WT:WhyType a}, forall (x:a), ~ (mem x (empty :(set a))). Parameter add: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> (set a). Axiom add_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a), forall (s:(set a)), (mem x (add y s)) <-> ((x = y) \/ (mem x s)). Parameter remove: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> (set a). Axiom remove_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a) (s:(set a)), (mem x (remove y s)) <-> ((~ (x = y)) /\ (mem x s)). Axiom subset_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set a)), (subset (remove x s) s). Parameter union: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set a). Axiom union_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a)) (s2:(set a)) (x:a), (mem x (union s1 s2)) <-> ((mem x s1) \/ (mem x s2)). Parameter inter: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set a). Axiom inter_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a)) (s2:(set a)) (x:a), (mem x (inter s1 s2)) <-> ((mem x s1) /\ (mem x s2)). Parameter diff: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set a). Axiom diff_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a)) (s2:(set a)) (x:a), (mem x (diff s1 s2)) <-> ((mem x s1) /\ ~ (mem x s2)). Axiom subset_diff : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a)) (s2:(set a)), (subset (diff s1 s2) s1). Parameter choose: forall {a:Type} {a_WT:WhyType a}, (set a) -> a. Axiom choose_def : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)), (~ (is_empty s)) -> (mem (choose s) s). Parameter cardinal: forall {a:Type} {a_WT:WhyType a}, (set a) -> Z. Axiom cardinal_nonneg : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)), (0%Z <= (cardinal s))%Z. Axiom cardinal_empty : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)), ((cardinal s) = 0%Z) <-> (is_empty s). Axiom cardinal_add : forall {a:Type} {a_WT:WhyType a}, forall (x:a), forall (s:(set a)), (~ (mem x s)) -> ((cardinal (add x s)) = (1%Z + (cardinal s))%Z). Axiom cardinal_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a), forall (s:(set a)), (mem x s) -> ((cardinal s) = (1%Z + (cardinal (remove x s)))%Z). Axiom cardinal_subset : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a)) (s2:(set a)), (subset s1 s2) -> ((cardinal s1) <= (cardinal s2))%Z. Axiom cardinal1 : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)), ((cardinal s) = 1%Z) -> forall (x:a), (mem x s) -> (x = (choose s)). Axiom map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, Type. Parameter map_WhyType : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, WhyType (map a b). Existing Instance map_WhyType. Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, (map a b) -> a -> b. Parameter set1: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, (map a b) -> a -> b -> (map a b). Axiom Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set1 m a1 b1) a2) = b1). Axiom Select_neq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set1 m a1 b1) a2) = (get m a2)). Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, b -> (map a b). Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1). Axiom vertex : Type. Parameter vertex_WhyType : WhyType vertex. Existing Instance vertex_WhyType. Parameter v: (set vertex). Parameter g_succ: vertex -> (set vertex). Axiom G_succ_sound : forall (x:vertex), (subset (g_succ x) v). Parameter weight: vertex -> vertex -> Z. Axiom Weight_nonneg : forall (x:vertex) (y:vertex), (0%Z <= (weight x y))%Z. (* Why3 assumption *) Definition min(m:vertex) (q:(set vertex)) (d:(map vertex Z)): Prop := (mem m q) /\ forall (x:vertex), (mem x q) -> ((get d m) <= (get d x))%Z. (* Why3 assumption *) Inductive path : vertex -> vertex -> Z -> Prop := | Path_nil : forall (x:vertex), (path x x 0%Z) | Path_cons : forall (x:vertex) (y:vertex) (z:vertex), forall (d:Z), (path x y d) -> ((mem z (g_succ y)) -> (path x z (d + (weight y z))%Z)). (* Why3 goal *) Theorem Length_nonneg : forall (x:vertex) (y:vertex), forall (d:Z), (path x y d) -> (0%Z <= d)%Z. induction 1; try omega. generalize (Weight_nonneg y z); omega. Qed.