Changeset 1062 for src/ASM/Util.ma


Ignore:
Timestamp:
Jul 11, 2011, 2:09:03 PM (8 years ago)
Author:
mulligan
Message:

separated jmeq and coercions from foldstuff.ma in order to fix the ongoing mess in util.ma surrounding reduce_strong

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Util.ma

    r1061 r1062  
    22include "basics/types.ma".
    33include "arithmetics/nat.ma".
     4
     5include "ASM/JMCoercions.ma".
    46
    57(* let's implement a daemon not used by automation *)
     
    1214 with precedence 10
    1315for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
     16
     17definition hd ≝
     18  λA: Type[0].
     19  λl: list A.
     20  λproof: 0 < |l|.
     21  match l return λx. 0 < |x| → A with
     22  [ nil ⇒ λnil_absrd. ?
     23  | cons hd tl ⇒ λcons_prf. hd
     24  ].
     25  normalize in nil_absrd;
     26  cases(not_le_Sn_O 0)
     27  #HYP
     28  cases(HYP nil_absrd)
     29qed.
     30
     31definition tail ≝
     32  λA: Type[0].
     33  λl: list A.
     34  λproof: 0 < |l|.
     35  match l return λx. 0 < |x| → list A with
     36  [ nil ⇒ λnil_absrd. ?
     37  | cons hd tl ⇒ λcons_prf. tl
     38  ].
     39  normalize in nil_absrd;
     40  cases(not_le_Sn_O 0)
     41  #HYP
     42  cases(HYP nil_absrd)
     43qed.
     44
     45let rec split
     46  (A: Type[0]) (l: list A) (index: nat) (proof: index < |l|)
     47    on index ≝
     48  match index return λx. x < |l| → (list A) × (list A) with
     49  [ O ⇒ λzero_prf. 〈[], l〉
     50  | S index' ⇒ λsucc_prf.
     51    match l return λx. S index' < |x| → (list A) × (list A) with
     52    [ nil ⇒ λnil_absrd. ?
     53    | cons hd tl ⇒ λcons_prf.
     54      let 〈l1, l2〉 ≝ split A tl index' ? in
     55        〈hd :: l1, l2〉
     56    ] succ_prf
     57  ] proof.
     58  [1: normalize in nil_absrd;
     59      cases(not_le_Sn_O (S index'))
     60      #HYP
     61      cases(HYP nil_absrd)
     62  |2: normalize in cons_prf;
     63      normalize
     64      @le_S_S_to_le
     65      assumption
     66  ]
     67qed.
    1468
    1569let rec nth_safe
     
    67121  ].
    68122
     123(*
    69124axiom reduce_strong:
    70125  ∀A: Type[0].
     
    72127  ∀right: list A.
    73128    Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) |.
    74 
    75 (*
     129*)
     130
     131include "ASM/FoldStuff.ma".
     132
    76133let rec reduce_strong
    77   (A: Type[0]) (left: list A) (right: list A) (prf: | left | = | right |) on left ≝
     134  (A: Type[0]) (left: list A) (right: list A) (prf: | left | = | right |) on left
     135  : Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) |  ≝
    78136  match left return λx. |x| = |right| → Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) | with
    79137  [ nil ⇒
     
    86144    [ nil ⇒ λcons_nil_absrd_prf. ?
    87145    | cons hd' tl' ⇒ λcons_cons_prf.
    88       let tail_call ≝ reduce_strong A tl tl' ? in ?
     146      let 〈commonl, commonr〉 ≝ eject … (reduce_strong A tl tl' ?) in ? (*
     147      [ dp clr their_proof ⇒ ? (*
     148        let 〈commonl, commonr〉 ≝ clr in ? *)
     149      ]*)
    89150    ]
    90151  ] prf.
     
    96157  | 3: normalize in cons_nil_absrd_prf;
    97158       destruct(cons_nil_absrd_prf)
     159  | 4:
    98160  ]
    99 qed.
    100 *)   
     161qed.
    101162 
    102163axiom reduce_length:
Note: See TracChangeset for help on using the changeset viewer.