Changeset 3591 for LTS/utils.ma


Ignore:
Timestamp:
Jul 20, 2015, 7:08:44 PM (4 years ago)
Author:
piccolo
Message:

stared pass stack to monostack, closed the first three proof obbligations of simulation conditions

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/utils.ma

    r3579 r3591  
    398398| cons x xs ⇒ match l2 with [nil ⇒ False | cons y ys ⇒ f x y ∧ All2 … f xs ys]
    399399].
     400
     401(* chop *)
     402
     403let rec chop (A : Type[0]) (l : list A) on l : list A ≝
     404match l with
     405[ nil ⇒ nil ?
     406| cons x xs ⇒ match xs with [ nil ⇒ nil ? | cons _ _ ⇒ x :: chop … xs]
     407].
     408
     409lemma chop_append_singleton : ∀A : Type[0].∀x : A.∀l : list A.chop ? (l@ [x]) = l.
     410#A #x #l elim l normalize // #y * normalize //
     411qed.
     412
     413lemma chop_mem : ∀A : Type[0].∀x : A.∀l : list A. mem … x (chop ? l) → mem … x l.
     414#A #x #l elim l [*] #y * [ normalize /2/] #z #zs #IH * [/2/] /3/
     415qed.
Note: See TracChangeset for help on using the changeset viewer.