Add Coq Core Lib

proof-libs/coq/coq/.gitignore

@@ -0,0 +1,7 @@
+*.vo*
+*.aux
+*.glob
+*.cache
+.Makefile.d
+Makefile
+Makefile.conf

proof-libs/coq/coq/_CoqProject

@@ -0,0 +1,41 @@
+-R src/ Core
+-arg -w
+-arg all
+
+./src/Core_Clone.v
+
+./src/Core_Marker.v
+
+./src/Core_Option.v
+./src/Core_Cmp.v
+
+./src/Core_Base_Int.v
+./src/Core_Base_Int_Base_spec.v
+./src/Core_Base_Int_Base_impl.v
+
+./src/Core_Coerce.v
+./src/Core_Convert.v
+
+./src/Core_Ops_Arith.v
+./src/Core_Ops_Bit.v
+
+./src/Core_Ops.v
+
+./src/Core_Int.v
+
+./src/Core_Base_Seq.v
+./src/Core_Base_Seq_Base_spec.v
+
+./src/Core_Panicking.v
+
+./src/Core_Base_Seq_Base_impl.v
+
+./src/Core_Primitive.v
+
+./src/Core_Base_Int_Number_conversion.v
+
+./src/Core_Array.v
+
+./src/Core_Intrinsics.v
+
+./src/Core_Num.v

proof-libs/coq/coq/src/Core_Array.v

@@ -0,0 +1,72 @@
+(* File automatically generated by Hacspec *)
+From Coq Require Import ZArith.
+Import List.ListNotations.
+Open Scope Z_scope.
+Open Scope bool_scope.
+Require Import String.
+
+
+From Core Require Import Core_Coerce (t_Abstraction).
+Export Core_Coerce (t_Abstraction).
+
+From Core Require Import Core_Coerce (t_Concretization).
+Export Core_Coerce (t_Concretization).
+
+
+From Core Require Import Core_Base_Int_Number_conversion.
+Export Core_Base_Int_Number_conversion.
+
+From Core Require Import Core_Base_Seq.
+Export Core_Base_Seq.
+
+From Core Require Import Core_Int.
+Export Core_Int.
+
+
+From Core Require Import Core_Cmp.
+Export Core_Cmp.
+
+From Core Require Import Core_Clone.
+Export Core_Clone.
+
+
+From Core Require Import Core_Primitive.
+Export Core_Primitive.
+
+Instance t_Clone_427868774 `{v_T : Type} `{v_N : t_usize} `{t_Sized v_T} `{t_Clone v_T} : t_Clone (t_Array (v_T) (v_N)) :=
+  {
+    t_Clone_f_clone := fun (self : t_Array (v_T) (v_N)) =>
+      Build_t_Array (t_Clone_f_clone (t_Array_f_v self));
+  }.
+
+Instance t_PartialEq_670168337 `{v_T : Type} `{v_N : t_usize} `{t_Sized v_T} `{t_Clone v_T} `{t_PartialEq v_T v_T} : t_PartialEq (t_Array (v_T) (v_N)) (t_Array (v_T) (v_N)) :=
+  {
+    t_PartialEq_f_eq := fun (self : t_Array (v_T) (v_N)) (other : t_Array (v_T) (v_N)) =>
+      t_PartialEq_f_eq (t_Clone_f_clone (t_Array_f_v self)) (t_Array_f_v other);
+    t_PartialEq_f_ne := fun (self : t_Array (v_T) (v_N)) (other : t_Array (v_T) (v_N)) =>
+      negb (t_PartialEq_f_eq (t_Clone_f_clone (t_Array_f_v self)) (t_Array_f_v other));
+  }.
+
+Definition impl_2__reverse `{v_T : Type} `{v_N : t_usize} `{t_Sized v_T} `{t_Clone v_T} (self : t_Array (v_T) (v_N)) : t_Array (v_T) (v_N) :=
+  Build_t_Array (impl_2__rev (t_Array_f_v self)).
+
+Lemma lt_usize_implies_hax_int (x : t_usize) (y : t_usize) :
+  t_PartialOrd_f_lt (x) (y) = true ->
+  t_PartialOrd_f_lt (t_From_f_from (x)) (t_From_f_from (y)) = true.
+Proof. Admitted.
+
+Lemma lift_usize_equality (x : t_HaxInt) (y : t_usize) :
+  t_PartialEq_f_eq (x) (t_From_f_from  y) = true ->
+  t_PartialEq_f_eq (t_From_f_from (x)) (y) = true.
+Proof. Admitted.
+
+Program Definition impl_2__index `{v_T : Type} `{v_N : t_usize} `{t_Sized v_T} `{t_Clone v_T} (self : t_Array (v_T) (v_N)) (i : t_usize) `{andb (t_PartialEq_f_eq (impl_2__len (t_Array_f_v self)) (t_From_f_from (v_N))) (t_PartialOrd_f_lt (i) (v_N)) = true} : v_T :=
+    impl_2__get_index (H1 := _) (t_Array_f_v self) (t_From_f_from (i)).
+Admit Obligations.
+
+Definition impl_2__new `{v_T : Type} `{v_N : t_usize} `{t_Sized v_T} `{t_Clone v_T} (x : v_T) : t_Array (v_T) (v_N) :=
+  Build_t_Array (impl_2__repeat (t_From_f_from (v_N)) (x)).
+
+Program Definition impl_2__set_index `{v_T : Type} `{v_N : t_usize} `{t_Sized v_T} `{t_Clone v_T} (self : t_Array (v_T) (v_N)) (i : t_usize) (t : v_T) `{andb (t_PartialEq_f_eq (impl_2__len (t_Array_f_v self)) (t_From_f_from (v_N))) (t_PartialOrd_f_lt (i) (v_N)) = true} : t_Array (v_T) (v_N) :=
+  Build_t_Array (impl_2__set_index (H1 := _) (t_Array_f_v self) (t_From_f_from (i)) (t)).
+Admit Obligations.

proof-libs/coq/coq/src/Core_Base_Int.v

@@ -0,0 +1,30 @@
+(* File automatically generated by Hacspec *)
+From Coq Require Import ZArith.
+Import List.ListNotations.
+Open Scope Z_scope.
+Open Scope bool_scope.
+Require Import String.
+
+(* NotImplementedYet *)
+
+(* NotImplementedYet *)
+
+(* NotImplementedYet *)
+
+Definition t_HaxInt : Type := N.
+Definition t_Positive : Type := positive.
+
+Notation "'t_POS'" := t_HaxInt.
+Notation "'t_POS_POS_ZERO'" := N0.
+Notation "'t_POS_POS_POS'" := Npos.
+
+Notation "'t_POSITIVE'" := t_Positive.
+Notation "'t_POSITIVE_POSITIVE_XH'" := xH.
+Notation "'t_POSITIVE_POSITIVE_XO'" := xO.
+Notation "'t_POSITIVE_POSITIVE_XI'" := xI.
+
+Definition t_Unary : Type := nat.
+
+Notation "'t_UNARY'" := t_Unary.
+Notation "'t_UNARY_UNARY_ZERO'" := O.
+Notation "'t_UNARY_UNARY_SUCC'" := S.