diff options
| author | Yishuai Li | 2018-08-30 21:01:21 -0400 |
|---|---|---|
| committer | Yishuai Li | 2019-09-01 02:10:00 -0400 |
| commit | ea23c93e33131216cff049a908a3e423dc704624 (patch) | |
| tree | 4984f22a853643fcf33add72b4b9042a7e3dcfad /theories/Init | |
| parent | 1f74267d7e4affe14dbafc1a6f1e6f3f465f75a8 (diff) | |
Vectors: lemmas about uncons and splitAt
Co-authored-by: Konstantinos Kallas <konstantinos.kallas@hotmail.com>
Diffstat (limited to 'theories/Init')
| -rw-r--r-- | theories/Init/Datatypes.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 1639115cbd..aff081df12 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -243,6 +243,17 @@ Proof. rewrite Hfst; rewrite Hsnd; reflexivity. Qed. +Lemma single_valued_projections : + forall (A B : Type) (a1 a2 : A) (b1 b2 : B), + (a1, b1) = (a2, b2) -> a1 = a2 /\ b1 = b2. +Proof with auto. + split; intros. + - replace a1 with (fst (a1, b1)); replace a2 with (fst (a2, b2))... + rewrite H... + - replace b1 with (snd (a1, b1)); replace b2 with (snd (a2, b2))... + rewrite H... +Qed. + Definition prod_uncurry (A B C:Type) (f:A * B -> C) (x:A) (y:B) : C := f (x,y). |