diff options
author | Frédéric Besson <frederic.besson@inria.fr> | 2016-09-07 10:28:07 +0200 |
---|---|---|
committer | Frédéric Besson <frederic.besson@inria.fr> | 2016-09-07 10:28:07 +0200 |
commit | 6e847be2a6846ab11996d2774b6bc507a342a626 (patch) | |
tree | 18ddfc166371881314a763d63ce9e51216fa98fe /plugins/micromega/VarMap.v | |
parent | 977e91d0aa5cfece962fc82e3fd42402918663c8 (diff) |
micromega : more robust generation of proof terms
- Assert a purely arihtmetic sub-goal that is proved independently by reflexion.
(This reduces the stress on the conversion test)
- Does not use 'abstract' anymore (more natural proof-term)
- Fix a parsing bug (certain terms in Prop where not recognized)
Diffstat (limited to 'plugins/micromega/VarMap.v')
-rw-r--r-- | plugins/micromega/VarMap.v | 29 |
1 files changed, 27 insertions, 2 deletions
diff --git a/plugins/micromega/VarMap.v b/plugins/micromega/VarMap.v index 4981ddb30..2d2c0bc77 100644 --- a/plugins/micromega/VarMap.v +++ b/plugins/micromega/VarMap.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -26,6 +26,7 @@ Set Implicit Arguments. *) Section MakeVarMap. + Variable A : Type. Variable default : A. @@ -46,5 +47,29 @@ Section MakeVarMap. end. -End MakeVarMap. + Fixpoint singleton (x:positive) (v : A) : t := + match x with + | xH => Leaf v + | xO p => Node (singleton p v) default Empty + | xI p => Node Empty default (singleton p v) + end. + + Fixpoint vm_add (x: positive) (v : A) (m : t) {struct m} : t := + match m with + | Empty => singleton x v + | Leaf vl => + match x with + | xH => Leaf v + | xO p => Node (singleton p v) vl Empty + | xI p => Node Empty vl (singleton p v) + end + | Node l o r => + match x with + | xH => Node l v r + | xI p => Node l o (vm_add p v r) + | xO p => Node (vm_add p v l) o r + end + end. + +End MakeVarMap. |