source: src/ASM/UtilBranch.ma @ 3363

Last change on this file since 3363 was 2702, checked in by sacerdot, 7 years ago
  1. proof closed in ASM/UtilBranch
  2. more passes integrated in the compiler.ma
  3. some work on commenting out broken proofs in linearise.ma
File size: 2.4 KB
Line 
1include "ASM/Util.ma".
2include "ASM/Arithmetic.ma".
3
4definition nat_of_bool: bool → nat ≝
5  λb: bool.
6  match b with
7  [ true ⇒ 1
8  | false ⇒ 0
9  ].
10
11lemma blah:
12  ∀n: nat.
13  ∀bv: BitVector n.
14  ∀buffer: nat.
15    nat_of_bitvector_aux n buffer bv = nat_of_bitvector n bv + (buffer * 2^n).
16  #n #bv elim bv
17  [1:
18    #buffer elim buffer try %
19    #buffer' #inductive_hypothesis
20    normalize <times_n_1 %
21  |2:
22    #n' #hd #tl #inductive_hypothesis
23    #buffer cases hd normalize
24    >inductive_hypothesis
25    >inductive_hypothesis
26    [1: change with (? + (2 * buffer + 1) * ?) in ⊢ (??%?);
27        >associative_plus in ⊢ (???%); @eq_f >commutative_plus
28        whd in ⊢ (??%?); @eq_f2 // >commutative_times in ⊢ (???(??%));
29        <associative_times //
30    | <plus_n_O normalize <plus_n_O @eq_f <associative_times
31      <commutative_times in ⊢ (???%); <associative_times //
32qed.
33
34lemma nat_of_bitvector_aux_hd_tl:
35  ∀n: nat.
36  ∀tl: BitVector n.
37  ∀hd: bool.
38    nat_of_bitvector (S n) (hd:::tl) =
39      nat_of_bitvector n tl + (nat_of_bool hd * 2^n).
40  #n #tl elim tl
41  [1:
42    #hd cases hd %
43  |2:
44    #n' #hd' #tl' #inductive_hypothesis #hd
45    cases hd whd in ⊢ (??%?); normalize nodelta
46    >inductive_hypothesis cases hd' normalize nodelta
47    normalize in match (nat_of_bool ?);
48    normalize in match (nat_of_bool ?);
49    [4:
50      normalize in match (2 * ?);
51      <plus_n_O <plus_n_O %
52    |3:
53      normalize in match (2 * ?);
54      normalize in match (0 + 1);
55      <plus_n_O
56      normalize in match (1 * ?);
57      <plus_n_O
58      cases daemon
59      (* XXX: lemma *)
60    |*:
61      cases daemon
62    ]
63  ]
64qed.
65
66lemma succ_nat_of_bitvector_aux_half_add_1:
67  ∀n: nat.
68  ∀bv: BitVector n.
69  ∀buffer: nat.
70  ∀power_proof: nat_of_bitvector … bv < 2^n - 1.
71    S (nat_of_bitvector_aux n buffer bv) =
72      nat_of_bitvector … (add n (bitvector_of_nat … 1) bv).
73  #n #bv elim bv
74  [1:
75    #buffer normalize #absurd
76    cases (lt_to_not_zero … absurd)
77  |2:
78    #n' #hd #tl #inductive_hypothesis #buffer
79    cases daemon
80  ]
81qed.
82   
83lemma succ_nat_of_bitvector_half_add_1:
84  ∀n: nat.
85  ∀bv: BitVector n.
86  ∀power_proof: nat_of_bitvector … bv < 2^n - 1.
87    S (nat_of_bitvector … bv) = nat_of_bitvector …
88      (add n (bitvector_of_nat … 1) bv).
89  #n #bv elim bv
90  [1:
91    normalize #absurd
92    cases (lt_to_not_zero … absurd)
93  |2:
94    #n' #hd #tl #inductive_hypothesis
95    cases daemon
96  ]
97qed.
Note: See TracBrowser for help on using the repository browser.