diff options
Diffstat (limited to 'plugins/micromega/Env.v')
| -rw-r--r-- | plugins/micromega/Env.v | 182 |
1 files changed, 182 insertions, 0 deletions
diff --git a/plugins/micromega/Env.v b/plugins/micromega/Env.v new file mode 100644 index 00000000..231004bc --- /dev/null +++ b/plugins/micromega/Env.v @@ -0,0 +1,182 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* *) +(* Micromega: A reflexive tactic using the Positivstellensatz *) +(* *) +(* Frédéric Besson (Irisa/Inria) 2006-2008 *) +(* *) +(************************************************************************) + +Require Import ZArith. +Require Import Coq.Arith.Max. +Require Import List. +Set Implicit Arguments. + +(* I have addded a Leaf constructor to the varmap data structure (/plugins/ring/Quote.v) + -- this is harmless and spares a lot of Empty. + This means smaller proof-terms. + BTW, by dropping the polymorphism, I get small (yet noticeable) speed-up. +*) + +Section S. + + Variable D :Type. + + Definition Env := positive -> D. + + Definition jump (j:positive) (e:Env) := fun x => e (Pplus x j). + + Definition nth (n:positive) (e : Env ) := e n. + + Definition hd (x:D) (e: Env) := nth xH e. + + Definition tail (e: Env) := jump xH e. + + Lemma psucc : forall p, (match p with + | xI y' => xO (Psucc y') + | xO y' => xI y' + | 1%positive => 2%positive + end) = (p+1)%positive. + Proof. + destruct p. + auto with zarith. + rewrite xI_succ_xO. + auto with zarith. + reflexivity. + Qed. + + Lemma jump_Pplus : forall i j l, + forall x, jump (i + j) l x = jump i (jump j l) x. + Proof. + unfold jump. + intros. + rewrite Pplus_assoc. + reflexivity. + Qed. + + Lemma jump_simpl : forall p l, + forall x, jump p l x = + match p with + | xH => tail l x + | xO p => jump p (jump p l) x + | xI p => jump p (jump p (tail l)) x + end. + Proof. + destruct p ; unfold tail ; intros ; repeat rewrite <- jump_Pplus. + (* xI p = p + p + 1 *) + rewrite xI_succ_xO. + rewrite Pplus_diag. + rewrite <- Pplus_one_succ_r. + reflexivity. + (* xO p = p + p *) + rewrite Pplus_diag. + reflexivity. + reflexivity. + Qed. + + Ltac jump_s := + repeat + match goal with + | |- context [jump xH ?e] => rewrite (jump_simpl xH) + | |- context [jump (xO ?p) ?e] => rewrite (jump_simpl (xO p)) + | |- context [jump (xI ?p) ?e] => rewrite (jump_simpl (xI p)) + end. + + Lemma jump_tl : forall j l, forall x, tail (jump j l) x = jump j (tail l) x. + Proof. + unfold tail. + intros. + repeat rewrite <- jump_Pplus. + rewrite Pplus_comm. + reflexivity. + Qed. + + Lemma jump_Psucc : forall j l, + forall x, (jump (Psucc j) l x) = (jump 1 (jump j l) x). + Proof. + intros. + rewrite <- jump_Pplus. + rewrite Pplus_one_succ_r. + rewrite Pplus_comm. + reflexivity. + Qed. + + Lemma jump_Pdouble_minus_one : forall i l, + forall x, (jump (Pdouble_minus_one i) (tail l)) x = (jump i (jump i l)) x. + Proof. + unfold tail. + intros. + repeat rewrite <- jump_Pplus. + rewrite <- Pplus_one_succ_r. + rewrite Psucc_o_double_minus_one_eq_xO. + rewrite Pplus_diag. + reflexivity. + Qed. + + Lemma jump_x0_tail : forall p l, forall x, jump (xO p) (tail l) x = jump (xI p) l x. + Proof. + intros. + unfold jump. + unfold tail. + unfold jump. + rewrite <- Pplus_assoc. + simpl. + reflexivity. + Qed. + + Lemma nth_spec : forall p l x, + nth p l = + match p with + | xH => hd x l + | xO p => nth p (jump p l) + | xI p => nth p (jump p (tail l)) + end. + Proof. + unfold nth. + destruct p. + intros. + unfold jump, tail. + unfold jump. + rewrite Pplus_diag. + rewrite xI_succ_xO. + simpl. + reflexivity. + unfold jump. + rewrite Pplus_diag. + reflexivity. + unfold hd. + unfold nth. + reflexivity. + Qed. + + + Lemma nth_jump : forall p l x, nth p (tail l) = hd x (jump p l). + Proof. + unfold tail. + unfold hd. + unfold jump. + unfold nth. + intros. + rewrite Pplus_comm. + reflexivity. + Qed. + + Lemma nth_Pdouble_minus_one : + forall p l, nth (Pdouble_minus_one p) (tail l) = nth p (jump p l). + Proof. + intros. + unfold tail. + unfold nth, jump. + rewrite Pplus_diag. + rewrite <- Psucc_o_double_minus_one_eq_xO. + rewrite Pplus_one_succ_r. + reflexivity. + Qed. + +End S. + |