Permalink
Find file
Fetching contributors…
Cannot retrieve contributors at this time
77 lines (68 sloc) 1.4 KB
Load "fin.tt";
Data Vect (A:*):(n:Nat)* where
vnil:Vect A O
| vcons:(k:Nat)(x:A)(xs:Vect A k)Vect A (S k);
vappend : (A:*)->(n,m:Nat)->(xs:Vect A n)->(ys:Vect A m)->
(Vect A (plus n m));
intros;
induction xs;
fill ys;
intros;
fill (vcons _ _ x xs_IH);
Qed;
vtail : (A:*)(k:Nat)(xs:Vect A (S k))Vect A k;
local vtailAux : (A:*)(k:Nat)(k':Nat)(xs:Vect A k')(p:Eq _ (S k) k')Vect A k;
Focus H;
intros;
refine (vtailAux _ k _ xs);
refine refl;
intro A k k' xs;
induction xs;
intros;
fill discriminate_Nat _ _ (sym _ _ _ p);
intros;
replace s_injective _ _ p0;
fill xs0;
Qed;
testvect = vcons _ _ (S O) (vnil Nat);
vectsum : (k:Nat)(v:Vect Nat k)Nat;
intros;
induction v;
fill O;
intros;
fill (plus x xs_IH);
Qed;
testvect2 = vcons _ _ (S O) (vcons _ _ (S (S (S O))) (vnil Nat));
testval2 = vectsum _ testvect2;
lookup:(A:*)(n:Nat)(i:Fin n)(xs:Vect A n)A;
local lookupAux:(A:*)(n:Nat)(i:Fin n)(n':Nat)(xs:Vect A n')(p:Eq _ n n')A;
intro A n i;
induction i;
intro k n' xs;
induction xs;
intros;
fill (discriminate_Nat _ _ (sym _ _ _ p));
intros;
fill x; {- fz (x::xs) -}
intro k i i_IH n' xs;
induction xs;
intros;
fill (discriminate_Nat _ _ (sym _ _ _ p0));
intros;
refine (i_IH k0);
fill xs0;
refine s_injective;
trivial;
intros;
refine (lookupAux _ _ i _ xs);
refine refl;
Qed;
lookupLt:(A:*)(n:Nat)(i:Nat)(p:Lt i n)(xs:Vect A n)A;
intros;
refine lookup;
fill n;
refine mkFin;
fill i;
fill p;
fill xs;
Qed;