diff options
author | Jason Gross <jgross@mit.edu> | 2017-06-11 19:05:01 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-06-11 19:05:01 -0400 |
commit | e8b12aeec4abea243b7f0be1100a6f33a6ca15ad (patch) | |
tree | 05bd86e9fcce8a6bca456eda6a5d9347a5a8391e /src/Util | |
parent | 9d049ecc47d6ac75301324dff1535bc757ac44d7 (diff) |
Add unfold lemmas for id_with_alt
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/IdfunWithAlt.v | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/src/Util/IdfunWithAlt.v b/src/Util/IdfunWithAlt.v index ed7a82ace..9754c5b24 100644 --- a/src/Util/IdfunWithAlt.v +++ b/src/Util/IdfunWithAlt.v @@ -42,3 +42,34 @@ Fixpoint id_tuple_with_alt_proof {A n} | O => id_with_alt_proof | S n' => id_tuple'_with_alt_proof end. + +Lemma unfold_id_with_alt {A} value value' + : @id_with_alt A value value' = value. +Proof. reflexivity. Qed. +Lemma unfold_id_with_alt_proof {A} value value' pf + : @id_with_alt_proof A value value' pf = value. +Proof. reflexivity. Qed. +Local Ltac t_ind n := + let IHn := fresh "IHn" in + induction n as [|n IHn]; cbn [id_tuple'_with_alt id_tuple'_with_alt_proof]; + first [ rewrite unfold_id_with_alt | rewrite unfold_id_with_alt_proof ]; + [ reflexivity + | rewrite IHn, <- surjective_pairing; reflexivity ]. +Lemma unfold_id_tuple'_with_alt {A n} value value' + : @id_tuple'_with_alt A n value value' = value. +Proof. t_ind n. Qed. +Lemma unfold_id_tuple'_with_alt_proof {A n} value value' pf + : @id_tuple'_with_alt_proof A n value value' pf = value. +Proof. t_ind n. Qed. +Lemma unfold_id_tuple_with_alt {A n} value value' + : @id_tuple_with_alt A n value value' = value. +Proof. + destruct n; cbn [id_tuple_with_alt]; + [ apply unfold_id_with_alt | apply unfold_id_tuple'_with_alt ]. +Qed. +Lemma unfold_id_tuple_with_alt_proof {A n} value value' pf + : @id_tuple_with_alt_proof A n value value' pf = value. +Proof. + destruct n; cbn [id_tuple_with_alt_proof]; + [ apply unfold_id_with_alt_proof | apply unfold_id_tuple'_with_alt_proof ]. +Qed. |