2015-06-19 13 views
5

Als Übung in Coq, ich versuche zu beweisen, dass die folgende Funktion ein Paar Listen gleicher Länge zurückgibt.Handhabung let in Hypothese

Require Import List. 

Fixpoint split (A B:Set)(x:list (A*B)) : (list A)*(list B) := 
match x with 
|nil => (nil, nil) 
|cons (a,b) x1 => let (ta, tb) := split A B x1 in (a::ta, b::tb) 
end. 

Theorem split_eq_len : forall (A B:Set)(x:list (A*B))(y:list A)(z:list B),(split A B x)=(y,z) -> length y = length z. 
Proof. 
intros A B x. 
elim x. 
simpl. 
intros y z. 
intros H. 
injection H. 
intros H1 H2. 
rewrite <- H1. 
rewrite <- H2. 
reflexivity. 
intros hx. 
elim hx. 
intros a b tx H y z. 
simpl. 
intro. 

Nach dem letzten Schritt erhalte ich eine Hypothese mit einer let Aussage innen, die ich weiß nicht, wie zu handhaben:

1 subgoals 
A : Set 
B : Set 
x : list (A * B) 
hx : A * B 
a : A 
b : B 
tx : list (A * B) 
H : forall (y : list A) (z : list B), 
    split A B tx = (y, z) -> length y = length z 
y : list A 
z : list B 
H0 : (let (ta, tb) := split A B tx in (a :: ta, b :: tb)) = (y, z) 
______________________________________(1/1) 
length y = length z 

Antwort

6

Sie wollen destruct (split A B tx) zu tun. Dies wird es aufbrechen und die beiden Teile an ta und tb

binden