From 7d220f8b61649646692983872626d6a8042446a9 Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 20 Mar 2009 01:22:58 +0000 Subject: Directory 'contrib' renamed into 'plugins', to end confusion with archive of user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/micromega/VarMap.v | 258 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 258 insertions(+) create mode 100644 plugins/micromega/VarMap.v (limited to 'plugins/micromega/VarMap.v') diff --git a/plugins/micromega/VarMap.v b/plugins/micromega/VarMap.v new file mode 100644 index 000000000..ed204d92b --- /dev/null +++ b/plugins/micromega/VarMap.v @@ -0,0 +1,258 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* t + | Node : t -> A -> t -> t . + + Fixpoint find (vm : t ) (p:positive) {struct vm} : A := + match vm with + | Empty => default + | Leaf i => i + | Node l e r => match p with + | xH => e + | xO p => find l p + | xI p => find r p + end + end. + + (* an off_map (a map with offset) offers the same functionalites as /plugins/setoid_ring/BinList.v - it is used in EnvRing.v *) +(* + Definition off_map := (option positive *t )%type. + + + + Definition jump (j:positive) (l:off_map ) := + let (o,m) := l in + match o with + | None => (Some j,m) + | Some j0 => (Some (j+j0)%positive,m) + end. + + Definition nth (n:positive) (l: off_map ) := + let (o,m) := l in + let idx := match o with + | None => n + | Some i => i + n + end%positive in + find idx m. + + + Definition hd (l:off_map) := nth xH l. + + + Definition tail (l:off_map ) := jump xH l. + + + 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, + (jump (i + j) l) = (jump i (jump j l)). + Proof. + unfold jump. + destruct l. + destruct o. + rewrite Pplus_assoc. + reflexivity. + reflexivity. + Qed. + + Lemma jump_simpl : forall p l, + jump p l = + match p with + | xH => tail l + | xO p => jump p (jump p l) + | xI p => jump p (jump p (tail l)) + 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, tail (jump j l) = jump j (tail l). + Proof. + unfold tail. + intros. + repeat rewrite <- jump_Pplus. + rewrite Pplus_comm. + reflexivity. + Qed. + + Lemma jump_Psucc : forall j l, + (jump (Psucc j) l) = (jump 1 (jump j l)). + Proof. + intros. + rewrite <- jump_Pplus. + rewrite Pplus_one_succ_r. + rewrite Pplus_comm. + reflexivity. + Qed. + + Lemma jump_Pdouble_minus_one : forall i l, + (jump (Pdouble_minus_one i) (tail l)) = (jump i (jump i l)). + 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, jump (xO p) (tail l) = jump (xI p) l. + Proof. + intros. + jump_s. + repeat rewrite <- jump_Pplus. + reflexivity. + Qed. + + + Lemma nth_spec : forall p l, + nth p l = + match p with + | xH => hd l + | xO p => nth p (jump p l) + | xI p => nth p (jump p (tail l)) + end. + Proof. + unfold nth. + destruct l. + destruct o. + simpl. + rewrite psucc. + destruct p. + replace (p0 + xI p)%positive with ((p + (p0 + 1) + p))%positive. + reflexivity. + rewrite xI_succ_xO. + rewrite Pplus_one_succ_r. + rewrite <- Pplus_diag. + rewrite Pplus_comm. + symmetry. + rewrite (Pplus_comm p0). + rewrite <- Pplus_assoc. + rewrite (Pplus_comm 1)%positive. + rewrite <- Pplus_assoc. + reflexivity. + (**) + replace ((p0 + xO p))%positive with (p + p0 + p)%positive. + reflexivity. + rewrite <- Pplus_diag. + rewrite <- Pplus_assoc. + rewrite Pplus_comm. + rewrite Pplus_assoc. + reflexivity. + reflexivity. + simpl. + destruct p. + rewrite xI_succ_xO. + rewrite Pplus_one_succ_r. + rewrite <- Pplus_diag. + symmetry. + rewrite Pplus_comm. + rewrite Pplus_assoc. + reflexivity. + rewrite Pplus_diag. + reflexivity. + reflexivity. + Qed. + + + Lemma nth_jump : forall p l, nth p (tail l) = hd (jump p l). + Proof. + destruct l. + unfold tail. + unfold hd. + unfold jump. + unfold nth. + destruct o. + symmetry. + rewrite Pplus_comm. + rewrite <- Pplus_assoc. + rewrite (Pplus_comm p0). + reflexivity. + 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. + destruct l. + unfold tail. + unfold nth, jump. + destruct o. + rewrite ((Pplus_comm p)). + rewrite <- (Pplus_assoc p0). + rewrite Pplus_diag. + rewrite <- Psucc_o_double_minus_one_eq_xO. + rewrite Pplus_one_succ_r. + rewrite (Pplus_comm (Pdouble_minus_one p)). + rewrite Pplus_assoc. + rewrite (Pplus_comm p0). + reflexivity. + rewrite <- Pplus_one_succ_l. + rewrite Psucc_o_double_minus_one_eq_xO. + rewrite Pplus_diag. + reflexivity. + Qed. + +*) + +End MakeVarMap. + -- cgit v1.2.3