From e12110637730d067c216abcc86185b761189b342 Mon Sep 17 00:00:00 2001
From: vblot <24938579+vblot@users.noreply.github.com>
Date: Fri, 28 May 2021 18:29:37 +0200
Subject: getting rid of native-coq (#95)

---
 src/versions/native/Structures_native.v | 59 ---------------------------------
 1 file changed, 59 deletions(-)
 delete mode 100644 src/versions/native/Structures_native.v

(limited to 'src/versions/native/Structures_native.v')

diff --git a/src/versions/native/Structures_native.v b/src/versions/native/Structures_native.v
deleted file mode 100644
index 47ae21f..0000000
--- a/src/versions/native/Structures_native.v
+++ /dev/null
@@ -1,59 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     SMTCoq                                                             *)
-(*     Copyright (C) 2011 - 2021                                          *)
-(*                                                                        *)
-(*     See file "AUTHORS" for the list of authors                         *)
-(*                                                                        *)
-(*   This file is distributed under the terms of the CeCILL-C licence     *)
-(*                                                                        *)
-(**************************************************************************)
-
-
-Require Import PArray.
-
-
-Section Trace.
-
-  (* We use [array array step] to allow bigger trace *)
-  Definition trace (step:Type) := array (array step).
-
-  Definition trace_to_list {step:Type} (t:trace step) : list step :=
-    PArray.fold_left (fun res a => List.app res (PArray.to_list a)) nil t.
-
-  Definition trace_length {step:Type} (t:trace step) : int :=
-    PArray.fold_left (fun l a => (l + (length a))%int63) 0%int63 t.
-
-  Definition trace_get {step:Type} (t:trace step) (i:int) : step :=
-    snd (PArray.fold_left (fun (jres:(option int) * step) a =>
-                        let (j,res) := jres in
-                        match j with
-                        | Some j' =>
-                          let l := length a in
-                          if (j' < l)%int63 then
-                            (None, get a j')
-                          else
-                            ((Some ((j' - l)%int63)),res)
-                        | None => (None,res)
-                        end
-                     ) (Some i, (get (get t 0) 0)) t).
-
-  Definition trace_fold {state step:Type} (transition: state -> step -> state) (s0:state) (t:trace step) :=
-    PArray.fold_left (PArray.fold_left transition) s0 t.
-
-  Lemma trace_fold_ind (state step : Type) (P : state -> Prop) (transition : state -> step -> state) (t : trace step)
-      (IH: forall (s0 : state) (i : int), (i < trace_length t)%int63 = true -> P s0 -> P (transition s0 (trace_get t i))) :
-      forall s0 : state, P s0 -> P (trace_fold transition s0 t).
-  Proof.
-    apply PArray.fold_left_ind.
-    intros a i Hi Ha.
-    apply PArray.fold_left_ind;trivial.
-    intros a0 i0 Hi0 Ha0.       (* IH applied to a0 and (sum of the lengths of the first i arrays + i0) *)
-  Admitted.
-
-End Trace.
-
-
-Definition nat_eqb := beq_nat.
-Definition nat_eqb_eq := beq_nat_true_iff.
-Definition nat_eqb_refl := NPeano.Nat.eqb_refl.
-- 
cgit