new example: Warshall algorithm

examples/in_progress/warshall_algorithm.mlw → examples/warshall_algorithm.mlw

@@ -2,7 +2,11 @@
 (** Warshall algorithm
 
     Computes the transitive closure of a graph implemented as a Boolean
-    matrix. *)
+    matrix.
+
+    Authors: Martin Clochard (École Normale Supérieure)
+             Jean-Christophe Filliâtre (CNRS)
+ *)
 
 module WarshallAlgorithm
 
@@ -22,9 +26,9 @@ module WarshallAlgorithm
   lemma weakening:
     forall m i j k1 k2. 0 <= k1 <= k2 ->
     path m i j k1 -> path m i j k2
-  
+
   lemma decomposition:
-    forall m i j k. 0 <= k /\ path m i j (k+1) ->
+    forall m k. 0 <= k -> forall i j. path m i j (k+1) ->
       (path m i j k \/ (path m i k k /\ path m k j k))
 
   let transitive_closure (m: matrix bool) : matrix bool

examples/warshall_algorithm/warshall_algorithm_WarshallAlgorithm_decomposition_1.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import BuiltIn.
+Require BuiltIn.
+Require int.Int.
+Require map.Map.
+
+(* Why3 assumption *)
+Definition unit := unit.
+
+Axiom qtmark : Type.
+Parameter qtmark_WhyType : WhyType qtmark.
+Existing Instance qtmark_WhyType.
+
+(* Why3 assumption *)
+Inductive matrix
+  (a:Type) :=
+  | mk_matrix : Z -> Z -> (map.Map.map Z (map.Map.map Z a)) -> matrix a.
+Axiom matrix_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (matrix a).
+Existing Instance matrix_WhyType.
+Implicit Arguments mk_matrix [[a]].
+
+(* Why3 assumption *)
+Definition elts {a:Type} {a_WT:WhyType a} (v:(matrix a)): (map.Map.map Z
+  (map.Map.map Z a)) := match v with
+  | (mk_matrix x x1 x2) => x2
+  end.
+
+(* Why3 assumption *)
+Definition columns {a:Type} {a_WT:WhyType a} (v:(matrix a)): Z :=
+  match v with
+  | (mk_matrix x x1 x2) => x1
+  end.
+
+(* Why3 assumption *)
+Definition rows {a:Type} {a_WT:WhyType a} (v:(matrix a)): Z :=
+  match v with
+  | (mk_matrix x x1 x2) => x
+  end.
+
+(* Why3 assumption *)
+Definition index := (Z* Z)%type.
+
+(* Why3 assumption *)
+Definition get {a:Type} {a_WT:WhyType a} (a1:(matrix a)) (i:(Z*
+  Z)%type): a :=
+  match i with
+  | (r, c) => (map.Map.get (map.Map.get (elts a1) r) c)
+  end.
+
+(* Why3 assumption *)
+Definition set {a:Type} {a_WT:WhyType a} (a1:(matrix a)) (i:(Z* Z)%type)
+  (v:a): (matrix a) :=
+  match i with
+  | (r, c) => (mk_matrix (rows a1) (columns a1) (map.Map.set (elts a1) r
+      (map.Map.set (map.Map.get (elts a1) r) c v)))
+  end.
+
+(* Why3 assumption *)
+Definition valid_index {a:Type} {a_WT:WhyType a} (a1:(matrix a)) (i:(Z*
+  Z)%type): Prop :=
+  match i with
+  | (r, c) => ((0%Z <= r)%Z /\ (r < (rows a1))%Z) /\ ((0%Z <= c)%Z /\
+      (c < (columns a1))%Z)
+  end.
+
+(* Why3 assumption *)
+Definition make {a:Type} {a_WT:WhyType a} (r:Z) (c:Z) (v:a): (matrix a) :=
+  (mk_matrix r c (map.Map.const (map.Map.const v: (map.Map.map Z
+  a)): (map.Map.map Z (map.Map.map Z a)))).
+
+(* Why3 assumption *)
+Inductive path: (matrix bool) -> Z -> Z -> Z -> Prop :=
+  | Path_empty : forall (m:(matrix bool)) (i:Z) (j:Z) (k:Z), ((get m (i,
+      j)) = true) -> (path m i j k)
+  | Path_cons : forall (m:(matrix bool)) (i:Z) (x:Z) (j:Z) (k:Z),
+      ((0%Z <= x)%Z /\ (x < k)%Z) -> ((path m i x k) -> ((path m x j k) ->
+      (path m i j k))).
+
+Axiom weakening : forall (m:(matrix bool)) (i:Z) (j:Z) (k1:Z) (k2:Z),
+  ((0%Z <= k1)%Z /\ (k1 <= k2)%Z) -> ((path m i j k1) -> (path m i j k2)).
+
+Hint Constructors path.
+
+(* Why3 goal *)
+Theorem decomposition : forall (m:(matrix bool)) (k:Z), (0%Z <= k)%Z ->
+  forall (i:Z) (j:Z), (path m i j (k + 1%Z)%Z) -> ((path m i j k) \/ ((path m
+  i k k) /\ (path m k j k))).
+(* Why3 intros m k h1 i j h2. *)
+intros m k hk i j h.
+remember (k+1)%Z as t in h.
+induction h.
+left; apply Path_empty; auto.
+subst k0; intuition.
+assert (case: (x=k \/ x < k)%Z) by omega. destruct case.
+subst; eauto.
+left; eauto.
+assert (case: (x=k \/ x < k)%Z) by omega. destruct case.
+subst x.
+right; eauto.
+right; eauto.
+assert (case: (x=k \/ x < k)%Z) by omega. destruct case.
+subst; eauto.
+right; eauto.
+Qed.
+

examples/warshall_algorithm/warshall_algorithm_WarshallAlgorithm_weakening_1.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import BuiltIn.
+Require BuiltIn.
+Require int.Int.
+Require map.Map.
+
+(* Why3 assumption *)
+Definition unit := unit.
+
+Axiom qtmark : Type.
+Parameter qtmark_WhyType : WhyType qtmark.
+Existing Instance qtmark_WhyType.
+
+(* Why3 assumption *)
+Inductive matrix
+  (a:Type) :=
+  | mk_matrix : Z -> Z -> (map.Map.map Z (map.Map.map Z a)) -> matrix a.
+Axiom matrix_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (matrix a).
+Existing Instance matrix_WhyType.
+Implicit Arguments mk_matrix [[a]].
+
+(* Why3 assumption *)
+Definition elts {a:Type} {a_WT:WhyType a} (v:(matrix a)): (map.Map.map Z
+  (map.Map.map Z a)) := match v with
+  | (mk_matrix x x1 x2) => x2
+  end.
+
+(* Why3 assumption *)
+Definition columns {a:Type} {a_WT:WhyType a} (v:(matrix a)): Z :=
+  match v with
+  | (mk_matrix x x1 x2) => x1
+  end.
+
+(* Why3 assumption *)
+Definition rows {a:Type} {a_WT:WhyType a} (v:(matrix a)): Z :=
+  match v with
+  | (mk_matrix x x1 x2) => x
+  end.
+
+(* Why3 assumption *)
+Definition index := (Z* Z)%type.
+
+(* Why3 assumption *)
+Definition get {a:Type} {a_WT:WhyType a} (a1:(matrix a)) (i:(Z*
+  Z)%type): a :=
+  match i with
+  | (r, c) => (map.Map.get (map.Map.get (elts a1) r) c)
+  end.
+
+(* Why3 assumption *)
+Definition set {a:Type} {a_WT:WhyType a} (a1:(matrix a)) (i:(Z* Z)%type)
+  (v:a): (matrix a) :=
+  match i with
+  | (r, c) => (mk_matrix (rows a1) (columns a1) (map.Map.set (elts a1) r
+      (map.Map.set (map.Map.get (elts a1) r) c v)))
+  end.
+
+(* Why3 assumption *)
+Definition valid_index {a:Type} {a_WT:WhyType a} (a1:(matrix a)) (i:(Z*
+  Z)%type): Prop :=
+  match i with
+  | (r, c) => ((0%Z <= r)%Z /\ (r < (rows a1))%Z) /\ ((0%Z <= c)%Z /\
+      (c < (columns a1))%Z)
+  end.
+
+(* Why3 assumption *)
+Definition make {a:Type} {a_WT:WhyType a} (r:Z) (c:Z) (v:a): (matrix a) :=
+  (mk_matrix r c (map.Map.const (map.Map.const v: (map.Map.map Z
+  a)): (map.Map.map Z (map.Map.map Z a)))).
+
+(* Why3 assumption *)
+Inductive path: (matrix bool) -> Z -> Z -> Z -> Prop :=
+  | Path_empty : forall (m:(matrix bool)) (i:Z) (j:Z) (k:Z), ((get m (i,
+      j)) = true) -> (path m i j k)
+  | Path_cons : forall (m:(matrix bool)) (i:Z) (x:Z) (j:Z) (k:Z),
+      ((0%Z <= x)%Z /\ (x < k)%Z) -> ((path m i x k) -> ((path m x j k) ->
+      (path m i j k))).
+
+(* Why3 goal *)
+Theorem weakening : forall (m:(matrix bool)) (i:Z) (j:Z) (k1:Z) (k2:Z),
+  ((0%Z <= k1)%Z /\ (k1 <= k2)%Z) -> ((path m i j k1) -> (path m i j k2)).
+intros m i j k1 k2 (h1,h2) h3.
+induction h3.
+apply Path_empty; auto.
+apply Path_cons with x; auto.
+omega.
+Qed.
+