diff options
| author | Hugo Herbelin | 2019-09-09 14:26:08 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-09-09 14:26:08 +0200 |
| commit | 02d9b435cfd0f688a3ace6fd0aefbf02f5102f5b (patch) | |
| tree | 21d1f59fce160b3c50381648a3b007d80c74c2f4 /theories/Init | |
| parent | 9ee962e7c18aebd214e3be4fda2c36f5e9c65405 (diff) | |
| parent | 016c22454c6745ac753d7e376c9f457d6e934114 (diff) | |
Merge PR #9379: Vectors: lemmas about uncons and splitAt
Reviewed-by: Zimmi48
Reviewed-by: herbelin
Diffstat (limited to 'theories/Init')
| -rw-r--r-- | theories/Init/Datatypes.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 3e0bf1d8ae..6984a7c2b6 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -243,6 +243,19 @@ Proof. rewrite Hfst; rewrite Hsnd; reflexivity. Qed. +Lemma pair_equal_spec : + forall (A B : Type) (a1 a2 : A) (b1 b2 : B), + (a1, b1) = (a2, b2) <-> a1 = a2 /\ b1 = b2. +Proof with auto. + split; intros. + - split. + + 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... + - destruct H; subst... +Qed. + Definition prod_uncurry (A B C:Type) (f:A * B -> C) (x:A) (y:B) : C := f (x,y). |