Changeset 1564

Timestamp:

Nov 25, 2011, 3:31:40 PM (8 years ago)

Author:

sacerdot

Message:

Commit where we use a dependently typed version of bigops.
I am now going to try to revert it to the standard version, so this
commit is to keep trace of the old version.

File:

• src/ASM/CostsProof.ma (modified) (3 diffs)

src/ASM/CostsProof.ma

@@ -520 +520 @@
  [ O ⇒ λ_. 0
  | S m ⇒ λH. bigplus0 n f m ? ] (refl … n).
- //
+ <H % (* Automation works, but finds an ugly proof that goes in the contexts
+         of later theorems *)
+qed.
+
+lemma bigplus_0: ∀n. n=0 → ∀f. bigplus n f = 0.
+ #n #E >E //
+qed.
+
+lemma bigplus0_extensional:
+ ∀b,f1,f2,n,K. (∀n,H. f1 n H = f2 n H) → bigplus0 b f1 n K = bigplus0 b f2 n K.
+ #b #f1 #f2 #n elim n //
+ #m #IH #K #ext normalize @eq_f2 [ @ext | @IH @ext ]
+qed.
+
+lemma bigplus_extensional:
+ ∀b,f1,f2. (∀n,H. f1 n H = f2 n H) → bigplus b f1 = bigplus b f2.
+ #b cases b // #n #f1 #f2 @bigplus0_extensional
+qed.
+
+(*CSC: !!!!!!!!!!!!!!!!!!!!!!! *)
+axiom pi_f: ∀b. ∀f: ∀n. n < b → nat. ∀n. ∀p1,p2: n < b. f n p1 = f n p2.
+
+axiom bigplus0_sum:
+ ∀b1,b2. ∀f:(∀n. n < b1+b2 → nat). ∀n,K.
+  bigplus0 (b1+b2) f n K =
+  if ltb n b1 then
+   bigplus0 b1 (λn,H. f n ?) n ?
+  else
+   bigplus b1 (λn,H. f n ?)  + bigplus0 b2 (λn,H. f (b1+n) ?) (n-b1) ?.
+ cases daemon
+qed.
+
+lemma bigplus_sum:
+ ∀b1,b2. ∀f:(∀n. n < b1+b2 → nat).
+  bigplus (b1+b2) f =
+  bigplus b1 (λn,H. f n ?) + bigplus b2 (λn,H. f (b1+n) ?).
+ [2: normalize in H ⊢ %; >plus_n_Sm @le_plus // (*CSC: Automation is lost here*)
+ |3: normalize in H ⊢ %; @(transitive_le ? b1) // (*CSC: here too*)
+ | #b1 #b2 lapply (refl … (b1+b2)) cases (b1+b2) in ⊢ (??%? → ?);
+   [ #E #f cut (b1=0) [//] #E1 >bigplus_0 [2://] >bigplus_0 [2://]
+     cut (b2=0) // #E2 >bigplus_0 //
+   | #n #E #f whd in ⊢ (??%?); >bigplus0_sum
+ 
+  #f cases b1
+   cases (b1+b2)
+ ]
 qed.
 
@@ -530 +575 @@
  ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
  ∀dom_codom:(∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
-   block_cost (code_memory … initial) cost_labels pc 2^16 =
-   lookup_present … k_pres).
+   block_cost (code_memory … initial) cost_labels pc 2^16 = lookup_present … k_pres).
   let ctrace ≝ compute_cost_trace_label_return … trace in
   compute_max_trace_label_return_cost … trace =
@@ -537 +581 @@
  [2: cases (nth_safe … i ctrace H) normalize #id * #id_pc #K
    lapply (codom_dom … K) #k_pres //
- | #cost_labels #costmap #initial #final #trace #codom_dom #dom_codom normalize nodelta
-   whd in match
+ | #cost_labels #costmap #initial #final #trace #codom_dom #dom_codom
+   cases trace
+   [ #sb #sa #tr whd in ⊢ (let ctrace ≝ % in ??%?);
+   | #si #sl #sf #tr1 #tr2 whd in ⊢ (let ctrace ≝ % in ??%?);
+   ]
 
 lemma