fixed Coq realization for seq.Seq (still WIP)

parent e73b3b1a
......@@ -16,48 +16,26 @@ 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).
exact (list a).
Defined.
Global Instance seq_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (seq a).
Proof.
intros.
repeat split.
exact nil.
intros a a_WT.
split.
exact (@nil a).
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))).
intros a a_WT.
exact (fix len l := match l with
| nil => 0 | cons _ t => 1 + len t end)%Z.
Defined.
Hint Unfold length.
......@@ -65,15 +43,16 @@ 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.
intros a a_WT.
induction s.
auto with *.
unfold length. fold length. omega.
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).
exact nil.
Defined.
(* Why3 goal *)
......@@ -85,8 +64,10 @@ 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)).
intros a (default, _) s i.
exact ((fix nth n l := match l with
| nil => default
| cons h t => if Zeq_bool n 0%Z then h else nth (n - 1)%Z t end) i s).
Defined.
(* Why3 assumption *)
......@@ -96,27 +77,62 @@ Definition infix_eqeq {a:Type} {a_WT:WhyType a} (s1:(seq a)) (s2:(seq
Notation "x == y" := (infix_eqeq x y) (at level 70, no associativity).
Lemma length_nonneg:
forall {a:Type} {a_WT:WhyType a} (s: seq a), (0 <= length s)%Z.
induction s.
auto with *.
unfold length. fold length. omega.
Qed.
(* 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? *)
intros a a_WT.
induction s1.
inversion 1.
destruct s2; auto.
unfold length in H0. fold length in H0.
generalize (length_nonneg s2); omega.
destruct s2.
inversion 1.
unfold length in H0. fold length in H0.
generalize (length_nonneg s1); omega.
inversion 1.
apply f_equal2.
assert (h: (0 <= 0 < length (a0 :: s1)%list)%Z).
unfold length. fold length.
generalize (length_nonneg s1); omega.
generalize (H1 0%Z h); clear H1.
unfold mixfix_lbrb. destruct a_WT. auto.
apply IHs1.
split.
unfold length in H0. fold length in H0. omega.
intros i hi.
assert (h: (0 <= i+1 < length (a0 :: s1)%list)%Z).
unfold length. fold length. omega.
generalize (H1 (i+1)%Z h); clear H1.
unfold mixfix_lbrb. destruct a_WT.
assert (Zeq_bool (i+1) 0 = false).
generalize (Zeq_is_eq_bool (i+1) 0).
case (Zeq_bool (i+1) 0); intuition.
omega.
destruct (Zeq_bool (i+1) 0).
discriminate H1.
replace (i+1-1)%Z with i by omega.
auto.
Qed.
(* 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).
intros a aWT x l.
exact (cons x l).
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 *.
intros a a_WT x s.
unfold length, cons. fold length; auto.
Qed.
(* Why3 goal *)
......@@ -124,9 +140,11 @@ 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).
(*
intros a (d,eq) x s i hi.
split; intros.
subst i. unfold mixfix_lbrb.
subst i. unfold mixfix_lbrb. auto.
unfold mixfix_lbrb. simpl.
destruct s.
unfold List.nth, default, elts; simpl; auto.
destruct s; unfold mixfix_lbrb; simpl.
......@@ -145,16 +163,19 @@ rewrite Zabs2Nat.inj_succ in Heqn.
injection Heqn; auto.
omega.
Qed.
*)
Admitted. (* TODO *)
(* 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).
intros a aWT s x.
exact (s ++ List.cons x nil)%list.
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.
......@@ -162,12 +183,15 @@ simpl Datatypes.length.
rewrite Nat2Z.inj_add.
auto with *.
Qed.
*)
Admitted. (* TODO *)
(* 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.
......@@ -189,6 +213,8 @@ rewrite (Zabs2Nat.id (Datatypes.length l)). omega.
subst i.
rewrite (Zabs2Nat.id (Datatypes.length l)). omega.
Qed.
*)
Admitted. (* TODO *)
(* Why3 goal *)
Definition mixfix_lb_dtdt_rb: forall {a:Type} {a_WT:WhyType a}, (seq a) ->
......@@ -220,19 +246,23 @@ Definition mixfix_lb_dtdtrb {a:Type} {a_WT:WhyType a} (s:(seq a)) (i:Z): (seq
(* 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).
intros a aWT s1 s2.
exact (s1 ++ s2)%list.
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.
*)
Admitted. (* TODO *)
(* Why3 goal *)
Lemma concat_get1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(seq a))
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment