examples/kmp/kmp_WP_KnuthMorrisPratt_next_is_maximal_1.v

   1 (* This file is generated by Why3's Coq driver *)
   2 (* Beware! Only edit allowed sections below    *)
   3 Require Import BuiltIn.
   4 Require BuiltIn.
   5 Require HighOrd.
   6 Require int.Int.
   7 Require map.Map.
   8
   9 (* Why3 assumption *)
  10 Inductive ref (a:Type) :=
  11   | ref'mk : a -> ref a.
  12 Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
  13 Existing Instance ref_WhyType.
  14 Arguments ref'mk {a}.
  15
  16 (* Why3 assumption *)
  17 Definition contents {a:Type} {a_WT:WhyType a} (v:ref a) : a :=
  18   match v with
  19   | ref'mk x => x
  20   end.
  21
  22 Axiom array : forall (a:Type), Type.
  23 Parameter array_WhyType :
  24   forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
  25 Existing Instance array_WhyType.
  26
  27 Parameter elts:
  28   forall {a:Type} {a_WT:WhyType a}, array a -> Numbers.BinNums.Z -> a.
  29
  30 Parameter length:
  31   forall {a:Type} {a_WT:WhyType a}, array a -> Numbers.BinNums.Z.
  32
  33 Axiom array'invariant :
  34   forall {a:Type} {a_WT:WhyType a},
  35   forall (self:array a), (0%Z <= (length self))%Z.
  36
  37 (* Why3 assumption *)
  38 Definition mixfix_lbrb {a:Type} {a_WT:WhyType a} (a1:array a)
  39     (i:Numbers.BinNums.Z) : a :=
  40   elts a1 i.
  41
  42 Parameter mixfix_lblsmnrb:
  43   forall {a:Type} {a_WT:WhyType a}, array a -> Numbers.BinNums.Z -> a ->
  44   array a.
  45
  46 Axiom mixfix_lblsmnrb'spec'0 :
  47   forall {a:Type} {a_WT:WhyType a},
  48   forall (a1:array a) (i:Numbers.BinNums.Z) (v:a),
  49   ((length (mixfix_lblsmnrb a1 i v)) = (length a1)).
  50
  51 Axiom mixfix_lblsmnrb'spec :
  52   forall {a:Type} {a_WT:WhyType a},
  53   forall (a1:array a) (i:Numbers.BinNums.Z) (v:a),
  54   ((elts (mixfix_lblsmnrb a1 i v)) = (map.Map.set (elts a1) i v)).
  55
  56 Parameter make:
  57   forall {a:Type} {a_WT:WhyType a}, Numbers.BinNums.Z -> a -> array a.
  58
  59 Axiom make_spec :
  60   forall {a:Type} {a_WT:WhyType a},
  61   forall (n:Numbers.BinNums.Z) (v:a), (0%Z <= n)%Z ->
  62   (forall (i:Numbers.BinNums.Z), (0%Z <= i)%Z /\ (i < n)%Z ->
  63    ((mixfix_lbrb (make n v) i) = v)) /\
  64   ((length (make n v)) = n).
  65
  66 Axiom char : Type.
  67 Parameter char_WhyType : WhyType char.
  68 Existing Instance char_WhyType.
  69
  70 (* Why3 assumption *)
  71 Definition matches (a1:array char) (i1:Numbers.BinNums.Z) (a2:array char)
  72     (i2:Numbers.BinNums.Z) (n:Numbers.BinNums.Z) : Prop :=
  73   ((0%Z <= i1)%Z /\ (i1 <= ((length a1) - n)%Z)%Z) /\
  74   ((0%Z <= i2)%Z /\ (i2 <= ((length a2) - n)%Z)%Z) /\
  75   (forall (i:Numbers.BinNums.Z), (0%Z <= i)%Z /\ (i < n)%Z ->
  76    ((mixfix_lbrb a1 (i1 + i)%Z) = (mixfix_lbrb a2 (i2 + i)%Z))).
  77
  78 Axiom matches_empty :
  79   forall (a1:array char) (a2:array char) (i1:Numbers.BinNums.Z)
  80     (i2:Numbers.BinNums.Z),
  81   (0%Z <= i1)%Z /\ (i1 <= (length a1))%Z ->
  82   (0%Z <= i2)%Z /\ (i2 <= (length a2))%Z -> matches a1 i1 a2 i2 0%Z.
  83
  84 Axiom matches_right_extension :
  85   forall (a1:array char) (a2:array char) (i1:Numbers.BinNums.Z)
  86     (i2:Numbers.BinNums.Z) (n:Numbers.BinNums.Z),
  87   matches a1 i1 a2 i2 n -> (i1 <= (((length a1) - n)%Z - 1%Z)%Z)%Z ->
  88   (i2 <= (((length a2) - n)%Z - 1%Z)%Z)%Z ->
  89   ((mixfix_lbrb a1 (i1 + n)%Z) = (mixfix_lbrb a2 (i2 + n)%Z)) ->
  90   matches a1 i1 a2 i2 (n + 1%Z)%Z.
  91
  92 Axiom matches_contradiction_at_first :
  93   forall (a1:array char) (a2:array char) (i1:Numbers.BinNums.Z)
  94     (i2:Numbers.BinNums.Z) (n:Numbers.BinNums.Z),
  95   (0%Z < n)%Z -> ~ ((mixfix_lbrb a1 i1) = (mixfix_lbrb a2 i2)) ->
  96   ~ matches a1 i1 a2 i2 n.
  97
  98 Axiom matches_contradiction_at_i :
  99   forall (a1:array char) (a2:array char) (i1:Numbers.BinNums.Z)
 100     (i2:Numbers.BinNums.Z) (i:Numbers.BinNums.Z) (n:Numbers.BinNums.Z),
 101   (0%Z < n)%Z -> (0%Z <= i)%Z /\ (i < n)%Z ->
 102   ~ ((mixfix_lbrb a1 (i1 + i)%Z) = (mixfix_lbrb a2 (i2 + i)%Z)) ->
 103   ~ matches a1 i1 a2 i2 n.
 104
 105 Axiom matches_right_weakening :
 106   forall (a1:array char) (a2:array char) (i1:Numbers.BinNums.Z)
 107     (i2:Numbers.BinNums.Z) (n:Numbers.BinNums.Z) (n':Numbers.BinNums.Z),
 108   matches a1 i1 a2 i2 n -> (n' < n)%Z -> matches a1 i1 a2 i2 n'.
 109
 110 Axiom matches_left_weakening :
 111   forall (a1:array char) (a2:array char) (i1:Numbers.BinNums.Z)
 112     (i2:Numbers.BinNums.Z) (n:Numbers.BinNums.Z) (n':Numbers.BinNums.Z),
 113   matches a1 (i1 - (n - n')%Z)%Z a2 (i2 - (n - n')%Z)%Z n -> (n' < n)%Z ->
 114   matches a1 i1 a2 i2 n'.
 115
 116 Axiom matches_sym :
 117   forall (a1:array char) (a2:array char) (i1:Numbers.BinNums.Z)
 118     (i2:Numbers.BinNums.Z) (n:Numbers.BinNums.Z),
 119   matches a1 i1 a2 i2 n -> matches a2 i2 a1 i1 n.
 120
 121 Axiom matches_trans :
 122   forall (a1:array char) (a2:array char) (a3:array char)
 123     (i1:Numbers.BinNums.Z) (i2:Numbers.BinNums.Z) (i3:Numbers.BinNums.Z)
 124     (n:Numbers.BinNums.Z),
 125   matches a1 i1 a2 i2 n -> matches a2 i2 a3 i3 n -> matches a1 i1 a3 i3 n.
 126
 127 (* Why3 assumption *)
 128 Definition is_next (p:array char) (j:Numbers.BinNums.Z)
 129     (n:Numbers.BinNums.Z) : Prop :=
 130   ((0%Z <= n)%Z /\ (n < j)%Z) /\
 131   matches p (j - n)%Z p 0%Z n /\
 132   (forall (z:Numbers.BinNums.Z), (n < z)%Z /\ (z < j)%Z ->
 133    ~ matches p (j - z)%Z p 0%Z z).
 134
 135 Axiom next_iteration :
 136   forall (p:array char) (a:array char) (i:Numbers.BinNums.Z)
 137     (j:Numbers.BinNums.Z) (n:Numbers.BinNums.Z),
 138   (0%Z < j)%Z /\ (j < (length p))%Z -> (j <= i)%Z /\ (i <= (length a))%Z ->
 139   matches a (i - j)%Z p 0%Z j -> is_next p j n -> matches a (i - n)%Z p 0%Z n.
 140
 141 Require Import Lia.
 142
 143 (* Why3 goal *)
 144 Theorem next_is_maximal :
 145   forall (p:array char) (a:array char) (i:Numbers.BinNums.Z)
 146     (j:Numbers.BinNums.Z) (n:Numbers.BinNums.Z) (k:Numbers.BinNums.Z),
 147   (0%Z < j)%Z /\ (j < (length p))%Z -> (j <= i)%Z /\ (i <= (length a))%Z ->
 148   ((i - j)%Z < k)%Z /\ (k < (i - n)%Z)%Z -> matches a (i - j)%Z p 0%Z j ->
 149   is_next p j n -> ~ matches a k p 0%Z (length p).
 150 (* Why3 intros p a i j n k (h1,h2) (h3,h4) (h5,h6) h7 h8. *)
 151 (* YOU MAY EDIT THE PROOF BELOW *)
 152 intros p a.
 153 intros i j n k Hj Hi Hk Hmatch Hnext.
 154 red.
 155  intro Hmax.
 156 elim Hnext; intros h1 (h2, h3).
 157 absurd (matches p (j - (i - k)) p 0 (i - k)).
 158 apply h3; lia.
 159 apply matches_trans with (a2 := a) (i2 := k).
 160 apply matches_sym.
 161 apply matches_left_weakening with (n := j).
 162 replace (k - (j - (i - k)))%Z with (i-j)%Z by ring.
 163  ring_simplify (j - (i - k) - (j - (i - k)))%Z.
 164  assumption.
 165 lia.
 166 apply matches_right_weakening with (n := length p).
 167 assumption.
 168 lia.
 169 Qed.
 170