aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega/Env.v
blob: caec7800c846081a35f5ddd9df53c61be7180e54 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
(*   \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 BinInt List.
Set Implicit Arguments.
Local Open Scope positive_scope.

Section S.

  Variable D :Type.

  Definition Env := positive -> D.

  Definition jump (j:positive) (e:Env) := fun x => e (x+j).

  Definition nth (n:positive) (e:Env) := e n.

  Definition hd (e:Env) := nth 1 e.

  Definition tail (e:Env) := jump 1 e.

  Lemma jump_add i j l x : jump (i + j) l x = jump i (jump j l) x.
  Proof.
    unfold jump. f_equal. apply Pos.add_assoc.
  Qed.

  Lemma jump_simpl p l 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; rewrite <- ?jump_add; f_equal;
    now rewrite Pos.add_diag.
  Qed.

  Lemma jump_tl j l x : tail (jump j l) x = jump j (tail l) x.
  Proof.
    unfold tail. rewrite <- !jump_add. f_equal. apply Pos.add_comm.
  Qed.

  Lemma jump_succ j l x : jump (Pos.succ j) l x = jump 1 (jump j l) x.
  Proof.
    rewrite <- jump_add. f_equal. symmetry. apply Pos.add_1_l.
  Qed.

  Lemma jump_pred_double i l x :
    jump (Pos.pred_double i) (tail l) x = jump i (jump i l) x.
  Proof.
    unfold tail. rewrite <- !jump_add. f_equal.
    now rewrite Pos.add_1_r, Pos.succ_pred_double, Pos.add_diag.
  Qed.

  Lemma nth_spec 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 hd, nth, tail, jump.
    destruct p; f_equal; now rewrite Pos.add_diag.
  Qed.

  Lemma nth_jump p l : nth p (tail l) = hd (jump p l).
  Proof.
    unfold hd, nth, tail, jump. f_equal. apply Pos.add_comm.
  Qed.

  Lemma nth_pred_double p l :
    nth (Pos.pred_double p) (tail l) = nth p (jump p l).
  Proof.
    unfold nth, tail, jump. f_equal.
    now rewrite Pos.add_1_r, Pos.succ_pred_double, Pos.add_diag.
  Qed.

End S.

Ltac jump_simpl :=
  repeat
    match goal with
      | |- appcontext [jump xH] => rewrite (jump_simpl xH)
      | |- appcontext [jump (xO ?p)] => rewrite (jump_simpl (xO p))
      | |- appcontext [jump (xI ?p)] => rewrite (jump_simpl (xI p))
    end.