diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-06-05 23:17:33 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-06-06 12:38:45 +0100 |
| commit | 1c8e0373d735ac88740f96c5da1d929ce3f7b688 (patch) | |
| tree | 60c170715bdc960778f58502f56dcb28775d3e13 /src/common | |
| parent | 34a0415ad0c65602ba097c37e23ced9cb3cf390e (diff) | |
| download | vericert-1c8e0373d735ac88740f96c5da1d929ce3f7b688.tar.gz vericert-1c8e0373d735ac88740f96c5da1d929ce3f7b688.zip | |
Move HTL renaming pass to own file
Diffstat (limited to 'src/common')
| -rw-r--r-- | src/common/Maps.v | 18 |
1 files changed, 17 insertions, 1 deletions
diff --git a/src/common/Maps.v b/src/common/Maps.v index 21a1d9e..3aa0b33 100644 --- a/src/common/Maps.v +++ b/src/common/Maps.v @@ -93,6 +93,22 @@ Definition contains (A: Type) (i: positive) (m: t A) : bool := | Some _ => true | None => false end. +End PTree. +Definition max_pc_map {A: Type} (m : Maps.PTree.t A) := + PTree.fold (fun m pc i => Pos.max m pc) m 1%positive. -End PTree. +Lemma max_pc_map_sound: + forall A m pc i, m!pc = Some i -> Ple pc (@max_pc_map A m). +Proof. + intros until i. unfold max_pc_map. + apply PTree_Properties.fold_rec with (P := fun c m => c!pc = Some i -> Ple pc m). + (* extensionality *) + intros. apply H0. rewrite H; auto. + (* base case *) + rewrite PTree.gempty. congruence. + (* inductive case *) + intros. rewrite PTree.gsspec in H2. destruct (peq pc k). + inv H2. xomega. + apply Ple_trans with a. auto. xomega. +Qed. |