1 files changed, 68 insertions, 0 deletions
diff --git a/plugins/micromega/DeclConstant.v b/plugins/micromega/DeclConstant.v
new file mode 100644
index 0000000000..47fcac6481
--- /dev/null
+++ b/plugins/micromega/DeclConstant.v
@@ -0,0 +1,68 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+(*                                                                      *)
+(* Micromega: A reflexive tactic using the Positivstellensatz           *)
+(*                                                                      *)
+(*  Frédéric Besson (Irisa/Inria) 2019                                  *)
+(*                                                                      *)
+(************************************************************************)
+
+(** Declaring 'allowed' terms using type classes.
+
+    Motivation: reification needs to know which terms are allowed.
+    For 'lia', the constant are only the integers built from Z0, Zpos, Zneg, xH, xO, xI.
+    However, if the term is ground it may be convertible to an integer.
+    Thus we could allow i.e. sqrt z for some integer z.
+
+    Proposal: for each type, the user declares using type-classes the set of allowed ground terms.
+ *)
+
+Require Import List.
+
+(**  Declarative definition of constants.
+     These are ground terms (without variables) of interest.
+     e.g. nat is built from O and S
+     NB: this does not need to be restricted to constructors.
+ *)
+
+(** Ground terms (see [GT] below) are built inductively from declared constants. *)
+
+Class DeclaredConstant {T : Type} (F : T).
+
+Class GT {T : Type} (F : T).
+
+Instance GT_O {T : Type} (F : T) {DC : DeclaredConstant F} : GT F.
+Defined.
+
+Instance GT_APP1 {T1 T2 : Type} (F : T1 -> T2) (A : T1) :
+  DeclaredConstant F ->
+  GT A -> GT (F A).
+Defined.
+
+Instance GT_APP2 {T1 T2 T3: Type} (F : T1 -> T2 -> T3)
+         {A1 : T1} {A2 : T2} {DC:DeclaredConstant F} :
+         GT A1 -> GT A2 -> GT (F A1 A2).
+Defined.
+
+Require Import ZArith.
+
+Instance DO : DeclaredConstant O := {}.
+Instance DS : DeclaredConstant S := {}.
+Instance DxH: DeclaredConstant xH := {}.
+Instance DxI: DeclaredConstant xI := {}.
+Instance DxO: DeclaredConstant xO := {}.
+Instance DZO: DeclaredConstant Z0 := {}.
+Instance DZpos: DeclaredConstant Zpos := {}.
+Instance DZneg: DeclaredConstant Zneg := {}.
+Instance DZpow_pos : DeclaredConstant Z.pow_pos := {}.
+
+Require Import QArith.
+
+Instance DQ : DeclaredConstant Qmake := {}.