diff options
| author |  Rutger Broekhoff | 2024-06-27 01:56:05 +0200 |
|---|---|---|
| committer | Rutger Broekhoff | 2024-06-27 01:56:05 +0200 |
| commit | 4598e77a9406d8040357c943a05dd1ab939932db (patch) | |
| tree | e990beaa94803da3585547f22e186e8819f6a887 /shared.v | |
| parent | 73df1945b31c0beee88cf4476df4ccd09d31403b (diff) | |
| download | mininix-formalization-4598e77a9406d8040357c943a05dd1ab939932db.tar.gz mininix-formalization-4598e77a9406d8040357c943a05dd1ab939932db.zip | |
Tidy up project
* Write README.md
* Add LICENSE
* Clean up some theorems and proofs
Diffstat (limited to 'shared.v')
| -rw-r--r-- | shared.v | 11 |
1 files changed, 5 insertions, 6 deletions
| @@ -14,12 +14,11 @@ Definition nonrecs : gmap string b_rhs → gmap string expr := | |||
| 14 | 14 | ||
| 15 | Lemma nonrecs_nonrec_fmap bs : nonrecs (B_Nonrec <$> bs) = bs. | 15 | Lemma nonrecs_nonrec_fmap bs : nonrecs (B_Nonrec <$> bs) = bs. |
| 16 | Proof. | 16 | Proof. |
| 17 | induction bs using map_ind. | 17 | induction bs using map_ind; [done|]. |
| 18 | - done. | 18 | unfold nonrecs. |
| 19 | - unfold nonrecs. | 19 | rewrite fmap_insert. |
| 20 | rewrite fmap_insert. | 20 | rewrite omap_insert_Some with (y := x); try done. |
| 21 | rewrite omap_insert_Some with (y := x); try done. | 21 | by f_equal. |
| 22 | by f_equal. | ||
| 23 | Qed. | 22 | Qed. |
| 24 | 23 | ||
| 25 | Lemma rec_subst_nonrec_fmap bs : rec_subst (B_Nonrec <$> bs) = bs. | 24 | Lemma rec_subst_nonrec_fmap bs : rec_subst (B_Nonrec <$> bs) = bs. |