Sequence.v 1.69 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below    *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require set.Set.
Require settheory.Interval.
Require settheory.Relation.
Require settheory.InverseDomRan.
Require settheory.Function.
Require settheory.Identity.

Import set.Set.
Open Scope Z_scope.

(* Why3 assumption *)
Definition seq_length {a:Type} {a_WT:WhyType a}(n:Z) (s:(set.Set.set
  a)): (set.Set.set (set.Set.set (Z* a)%type)) :=
  (settheory.Function.infix_mnmngt (settheory.Interval.mk 1%Z n) s).

(* Why3 goal *)
Definition seq: forall {a:Type} {a_WT:WhyType a}, (set.Set.set a) ->
  (set.Set.set (set.Set.set (Z* a)%type)).
intros a a_WT s.
exact (fun f => exists n:Z, 0 <= n /\ mem f (seq_length n s)).
Defined.

(* Why3 goal *)
Definition size: forall {a:Type} {a_WT:WhyType a}, (set.Set.set (Z*
  a)%type) -> Z.

Defined.

(* Why3 goal *)
Lemma mem_seq : forall {a:Type} {a_WT:WhyType a}, forall (s:(set.Set.set a))
  (r:(set.Set.set (Z* a)%type)), (set.Set.mem r (seq s)) <->
  ((0%Z <= (size r))%Z /\ (set.Set.mem r (seq_length (size r) s))).
intros a a_WT s r.

Qed.

(* Why3 goal *)
Lemma seq_as_total_function : forall {a:Type} {a_WT:WhyType a},
  forall (s:(set.Set.set a)) (r:(set.Set.set (Z* a)%type)), (set.Set.mem r
  (seq s)) -> (set.Set.mem r
  (settheory.Function.infix_mnmngt (settheory.Interval.mk 1%Z (size r)) s)).
intros a a_WT s r h1.

Qed.

(* Why3 goal *)
Lemma size_def : forall {a:Type} {a_WT:WhyType a}, forall (n:Z)
  (r:(set.Set.set (Z* a)%type)), ((size r) = n) <-> exists s:(set.Set.set a),
  (set.Set.mem r (seq_length n s)).
intros a a_WT n r.

Qed.


(* Unused content named mem_seq_length
intros a a_WT n s.

Qed.
 *)