Coq realization for theory seq.Seq (WIP)

Makefile.in

@@ -865,18 +865,22 @@ COQLIBS_LIST = $(addprefix lib/coq/list/, $(COQLIBS_LIST_FILES))
 COQLIBS_OPTION_FILES = Option
 COQLIBS_OPTION = $(addprefix lib/coq/option/, $(COQLIBS_OPTION_FILES))
 
+COQLIBS_SEQ_FILES = Seq
+COQLIBS_SEQ = $(addprefix lib/coq/seq/, $(COQLIBS_SEQ_FILES))
+
 ifeq (@enable_coq_fp_libs@,yes)
 COQLIBS_FP_FILES = Rounding SingleFormat Single DoubleFormat Double
 COQLIBS_FP_ALL_FILES = GenFloat $(COQLIBS_FP_FILES)
 COQLIBS_FP = $(addprefix lib/coq/floating_point/, $(COQLIBS_FP_ALL_FILES))
 endif
 
-COQLIBS_FILES = lib/coq/BuiltIn $(COQLIBS_INT) $(COQLIBS_BOOL) $(COQLIBS_REAL) $(COQLIBS_NUMBER) $(COQLIBS_SET) $(COQLIBS_MAP) $(COQLIBS_LIST) $(COQLIBS_OPTION) $(COQLIBS_FP)
+COQLIBS_FILES = lib/coq/BuiltIn lib/coq/HighOrd $(COQLIBS_INT) $(COQLIBS_BOOL) $(COQLIBS_REAL) $(COQLIBS_NUMBER) $(COQLIBS_SET) $(COQLIBS_MAP) $(COQLIBS_LIST) $(COQLIBS_OPTION) $(COQLIBS_SEQ) $(COQLIBS_FP)
 
 drivers/coq-realizations.aux: Makefile
 	$(if $(QUIET),@echo 'Generate $@' &&) \
 	(echo "(* generated automatically at compilation time *)"; \
 	echo 'theory BuiltIn meta "realized_theory" "BuiltIn", "" end'; \
+	echo 'theory HighOrd meta "realized_theory" "HighOrd", "" end'; \
 	for f in $(COQLIBS_INT_FILES); do \
 	echo 'theory int.'"$$f"' meta "realized_theory" "int.'"$$f"'", "" end'; done; \
 	for f in $(COQLIBS_BOOL_FILES); do \
@@ -893,13 +897,15 @@ drivers/coq-realizations.aux: Makefile
 	echo 'theory list.'"$$f"' meta "realized_theory" "list.'"$$f"'", "" end'; done; \
 	for f in $(COQLIBS_OPTION_FILES); do \
 	echo 'theory option.'"$$f"' meta "realized_theory" "option.'"$$f"'", "" end'; done; \
+	for f in $(COQLIBS_SEQ_FILES); do \
+	echo 'theory seq.'"$$f"' meta "realized_theory" "seq.'"$$f"'", "" end'; done; \
 	for f in $(COQLIBS_FP_FILES); do \
 	echo 'theory floating_point.'"$$f"' meta "realized_theory" "floating_point.'"$$f"'", "" end'; done; \
 	) > $@
 
 install_no_local::
 	mkdir -p $(LIBDIR)/why3/coq
-	cp lib/coq/BuiltIn.vo $(LIBDIR)/why3/coq/
+	cp lib/coq/BuiltIn.vo lib/coq/HighOrd.vo $(LIBDIR)/why3/coq/
 	mkdir -p $(LIBDIR)/why3/coq/int
 	cp $(addsuffix .vo, $(COQLIBS_INT)) $(LIBDIR)/why3/coq/int/
 	mkdir -p $(LIBDIR)/why3/coq/bool
@@ -916,6 +922,8 @@ install_no_local::
 	cp $(addsuffix .vo, $(COQLIBS_LIST)) $(LIBDIR)/why3/coq/list/
 	mkdir -p $(LIBDIR)/why3/coq/option
 	cp $(addsuffix .vo, $(COQLIBS_OPTION)) $(LIBDIR)/why3/coq/option/
+	mkdir -p $(LIBDIR)/why3/coq/seq
+	cp $(addsuffix .vo, $(COQLIBS_SEQ)) $(LIBDIR)/why3/coq/seq/
 ifeq (@enable_coq_fp_libs@,yes)
 	mkdir -p $(LIBDIR)/why3/coq/floating_point
 	cp $(addsuffix .vo, $(COQLIBS_FP)) $(LIBDIR)/why3/coq/floating_point/
@@ -947,6 +955,9 @@ update-coq-list: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theori
 update-coq-option: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/option.why
 	for f in $(COQLIBS_OPTION_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T option.$$f -o lib/coq/option/; done
 
+update-coq-seq: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/seq.why
+	for f in $(COQLIBS_SEQ_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T seq.$$f -o lib/coq/seq/; done
+
 update-coq-fp: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/floating_point.why
 	for f in $(COQLIBS_FP_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T floating_point.$$f -o lib/coq/floating_point/; done
 
@@ -955,7 +966,7 @@ else
 drivers/coq-realizations.aux:
 	echo "(* generated automatically at compilation time *)" > $@
 
-COQLIBS_FILES = lib/coq/BuiltIn
+COQLIBS_FILES = lib/coq/BuiltIn lib/coq/HighOrd
 
 endif
 
@@ -1625,6 +1636,7 @@ STDLIBS = algebra \
 	map \
 	number \
 	option \
+	seq \
 	pigeon \
 	real \
 	relations \

lib/coq/HighOrd.v

+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
+(*                                                                  *)
+(*  This software is distributed under the terms of the GNU Lesser  *)
+(*  General Public License version 2.1, with the special exception  *)
+(*  on linking described in file LICENSE.                           *)
+(*                                                                  *)
+(********************************************************************)
+
+Require Import BuiltIn.
+
+Definition func : forall (a:Type) (b:Type), Type.
+intros a b.
+exact (a -> b).
+Defined.
+
+Definition infix_at: forall {a:Type} {a_WT:WhyType a}
+  {b:Type} {b_WT:WhyType b}, (a -> b) -> a -> b.
+intros a aWT b bWT f x.
+exact (f x).
+Defined.
+
+Definition pred (a: Type) := func a bool.

lib/coq/seq/Seq.v

+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
+(*                                                                  *)
+(*  This software is distributed under the terms of the GNU Lesser  *)
+(*  General Public License version 2.1, with the special exception  *)
+(*  on linking described in file LICENSE.                           *)
+(*                                                                  *)
+(********************************************************************)
+
+(* This file is generated by Why3's Coq-realize driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import BuiltIn.
+Require BuiltIn.
+Require HighOrd.
+Require int.Int.
+
+(* This file is generated by Why3's Coq-realize driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import BuiltIn.
+Require BuiltIn.
+Require HighOrd.
+Require int.Int.
+
+(* This file is generated by Why3's Coq-realize driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import BuiltIn.
+Require BuiltIn.
+Require HighOrd.
+Require int.Int.
+
+Record _seq (a: Type) := {
+  elts: list a;
+  default: a
+}.
+
+(* Why3 goal *)
+Definition seq : forall (a:Type), Type.
+intro a.
+exact (_seq a).
+Defined.
+
+Global Instance seq_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (seq a).
+Proof.
+intros.
+repeat split.
+exact nil.
+destruct a_WT.
+exact why_inhabitant.
+decide equality.
+exact (why_decidable_eq default0 default1).
+decide equality.
+exact (why_decidable_eq a0 a1).
+Qed.
+
+(* Why3 goal *)
+Definition length: forall {a:Type} {a_WT:WhyType a}, (seq a) -> Z.
+intros.
+exact (Z_of_nat (length (elts _ X))).
+Defined.
+
+Hint Unfold length.
+
+(* Why3 goal *)
+Lemma length_nonnegative : forall {a:Type} {a_WT:WhyType a}, forall (s:(seq
+  a)), (0%Z <= (length s))%Z.
+intros a a_WT s.
+unfold length; simpl.
+auto with *.
+Qed.
+
+(* Why3 goal *)
+Definition empty: forall {a:Type} {a_WT:WhyType a}, (seq a).
+intros a a_WT.
+exact (Build__seq a nil why_inhabitant).
+Defined.
+
+(* Why3 goal *)
+Lemma empty_length : forall {a:Type} {a_WT:WhyType a}, ((length (empty : (seq
+  a))) = 0%Z).
+intros a a_WT.
+auto with *.
+Qed.
+
+(* Why3 goal *)
+Definition mixfix_lbrb: forall {a:Type} {a_WT:WhyType a}, (seq a) -> Z -> a.
+intros a aWT s i.
+exact (List.nth (Zabs_nat i) (elts _ s) (default _ s)).
+Defined.
+
+(* Why3 assumption *)
+Definition infix_eqeq {a:Type} {a_WT:WhyType a} (s1:(seq a)) (s2:(seq
+  a)): Prop := ((length s1) = (length s2)) /\ forall (i:Z), ((0%Z <= i)%Z /\
+  (i < (length s1))%Z) -> ((mixfix_lbrb s1 i) = (mixfix_lbrb s2 i)).
+
+Notation "x == y" := (infix_eqeq x y) (at level 70, no associativity).
+
+(* Why3 goal *)
+Lemma extensionality : forall {a:Type} {a_WT:WhyType a}, forall (s1:(seq a))
+  (s2:(seq a)), (infix_eqeq s1 s2) -> (s1 = s2).
+intros a a_WT s1 s2 h1.
+Admitted. (* FIXME: load a Coq library for this? *)
+
+(* Why3 goal *)
+Definition cons: forall {a:Type} {a_WT:WhyType a}, a -> (seq a) -> (seq a).
+intros a aWT x (l, d).
+exact (Build__seq a (cons x l) d).
+Defined.
+
+(* Why3 goal *)
+Lemma cons_length : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(seq
+  a)), ((length (cons x s)) = (1%Z + (length s))%Z).
+intros a a_WT x (l, d).
+unfold length, cons, elts.
+simpl Datatypes.length.
+simpl Z.of_nat.
+rewrite Zpos_P_of_succ_nat.
+auto with *.
+Qed.
+
+(* Why3 goal *)
+Lemma cons_get : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(seq a))
+  (i:Z), ((0%Z <= i)%Z /\ (i <= (length s))%Z) -> (((i = 0%Z) ->
+  ((mixfix_lbrb (cons x s) i) = x)) /\ ((~ (i = 0%Z)) ->
+  ((mixfix_lbrb (cons x s) i) = (mixfix_lbrb s (i - 1%Z)%Z)))).
+intros a a_WT x s i (h1,h2).
+split; intros.
+subst i. unfold mixfix_lbrb.
+destruct s.
+unfold List.nth, default, elts; simpl; auto.
+destruct s; unfold mixfix_lbrb; simpl.
+destruct (Z.abs_nat i) eqn:?.
+(* i = 0 *)
+assert (i = 0)%Z.
+assert (O < Z.abs_nat i)%nat.
+rewrite <- Zabs2Nat.inj_0.
+apply Zabs_nat_lt. omega. omega. omega.
+(* i = S n *)
+replace (Z.abs_nat (i - 1)) with n.
+reflexivity.
+assert (i = Zsucc (i-1))%Z by omega.
+rewrite H0 in Heqn.
+rewrite Zabs2Nat.inj_succ in Heqn.
+injection Heqn; auto.
+omega.
+Qed.
+
+(* Why3 goal *)
+Definition snoc: forall {a:Type} {a_WT:WhyType a}, (seq a) -> a -> (seq a).
+intros a aWT (l, d) x.
+exact (Build__seq a (l ++ List.cons x nil) d).
+Defined.
+
+(* Why3 goal *)
+Lemma snoc_length : forall {a:Type} {a_WT:WhyType a}, forall (s:(seq a))
+  (x:a), ((length (snoc s x)) = (1%Z + (length s))%Z).
+intros a a_WT (l, d) x.
+unfold length, snoc, elts.
+rewrite List.app_length.
+simpl Datatypes.length.
+rewrite Nat2Z.inj_add.
+auto with *.
+Qed.
+
+(* Why3 goal *)
+Lemma snoc_get : forall {a:Type} {a_WT:WhyType a}, forall (s:(seq a)) (x:a)
+  (i:Z), ((0%Z <= i)%Z /\ (i <= (length s))%Z) -> (((i < (length s))%Z ->
+  ((mixfix_lbrb (snoc s x) i) = (mixfix_lbrb s i))) /\
+  ((~ (i < (length s))%Z) -> ((mixfix_lbrb (snoc s x) i) = x))).
+intros a a_WT (l, d) x i (h1,h2).
+split; intros.
+unfold mixfix_lbrb.
+unfold default, elts; simpl; auto.
+unfold length in *; simpl in *.
+apply List.app_nth1.
+rewrite <- (Zabs2Nat.id (Datatypes.length l)).
+apply Zabs_nat_lt. omega.
+unfold mixfix_lbrb.
+unfold default, elts; simpl; auto.
+unfold length in *; simpl in *.
+assert (i = Z.of_nat (Datatypes.length l)).
+omega.
+rewrite List.app_nth2.
+replace (Z.abs_nat i - Datatypes.length l) with O.
+auto.
+subst i.
+rewrite (Zabs2Nat.id (Datatypes.length l)). omega.
+subst i.
+rewrite (Zabs2Nat.id (Datatypes.length l)). omega.
+Qed.
+
+(* Why3 goal *)
+Definition mixfix_lb_dtdt_rb: forall {a:Type} {a_WT:WhyType a}, (seq a) ->
+  Z -> Z -> (seq a).
+
+Admitted. (* TODO *)
+
+(* Why3 goal *)
+Lemma sub_length : forall {a:Type} {a_WT:WhyType a}, forall (s:(seq a)) (i:Z)
+  (j:Z), ((0%Z <= i)%Z /\ ((i <= j)%Z /\ (j <= (length s))%Z)) ->
+  ((length (mixfix_lb_dtdt_rb s i j)) = (j - i)%Z).
+intros a a_WT s i j (h1,(h2,h3)).
+
+Admitted. (* TODO *)
+
+(* Why3 goal *)
+Lemma sub_get : forall {a:Type} {a_WT:WhyType a}, forall (s:(seq a)) (i:Z)
+  (j:Z), ((0%Z <= i)%Z /\ ((i <= j)%Z /\ (j <= (length s))%Z)) ->
+  forall (k:Z), ((0%Z <= k)%Z /\ (k < (j - i)%Z)%Z) ->
+  ((mixfix_lbrb (mixfix_lb_dtdt_rb s i j) k) = (mixfix_lbrb s (i + k)%Z)).
+intros a a_WT s i j (h1,(h2,h3)) k (h4,h5).
+
+Admitted. (* TODO *)
+
+(* Why3 assumption *)
+Definition mixfix_lb_dtdtrb {a:Type} {a_WT:WhyType a} (s:(seq a)) (i:Z): (seq
+  a) := (mixfix_lb_dtdt_rb s i (length s)).
+
+(* Why3 goal *)
+Definition infix_plpl: forall {a:Type} {a_WT:WhyType a}, (seq a) -> (seq
+  a) -> (seq a).
+intros a aWT (l1, d1) (l2, d2).
+exact (Build__seq _ (l1 ++ l2) d1).
+Defined.
+
+(* Why3 goal *)
+Lemma concat_length : forall {a:Type} {a_WT:WhyType a}, forall (s1:(seq a))
+  (s2:(seq a)), ((length (infix_plpl s1
+  s2)) = ((length s1) + (length s2))%Z).
+intros a a_WT (l1,d1) (l2,d2).
+unfold length; simpl.
+rewrite List.app_length.
+rewrite Nat2Z.inj_add. auto.
+Qed.
+
+(* Why3 goal *)
+Lemma concat_get1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(seq a))
+  (s2:(seq a)) (i:Z), ((0%Z <= i)%Z /\ (i < (length s1))%Z) ->
+  ((mixfix_lbrb (infix_plpl s1 s2) i) = (mixfix_lbrb s1 i)).
+intros a a_WT s1 s2 i (h1,h2).
+
+Admitted. (* TODO *)
+
+(* Why3 goal *)
+Lemma concat_get2 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(seq a))
+  (s2:(seq a)) (i:Z), (((length s1) <= i)%Z /\
+  (i < ((length s1) + (length s2))%Z)%Z) -> ((mixfix_lbrb (infix_plpl s1 s2)
+  i) = (mixfix_lbrb s2 (i - (length s1))%Z)).
+intros a a_WT s1 s2 i (h1,h2).
+
+Admitted. (* TODO *)
+
+(* Why3 goal *)
+Definition create: forall {a:Type} {a_WT:WhyType a}, Z -> (Z -> a) -> (seq
+  a).
+
+Admitted. (* TODO *)
+
+(* Why3 goal *)
+Lemma create_length : forall {a:Type} {a_WT:WhyType a}, forall (len:Z)
+  (f:(Z -> a)), (0%Z <= len)%Z -> ((length (create len f)) = len).
+intros a a_WT len f h1.
+
+Admitted. (* TODO *)
+
+(* Why3 goal *)
+Lemma create_get : forall {a:Type} {a_WT:WhyType a}, forall (len:Z) (f:(Z ->
+  a)) (i:Z), ((0%Z <= i)%Z /\ (i < len)%Z) -> ((mixfix_lbrb (create len f)
+  i) = (f i)).
+intros a a_WT len f i (h1,h2).
+
+Admitted. (* TODO *)
+