diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/Coqlib.v | 41 | ||||
| -rw-r--r-- | lib/Floats.v | 63 | ||||
| -rw-r--r-- | lib/HashedSet.v | 1414 | ||||
| -rw-r--r-- | lib/HashedSetaux.ml | 67 | ||||
| -rw-r--r-- | lib/HashedSetaux.mli | 18 | ||||
| -rw-r--r-- | lib/Impure/ImpConfig.v | 85 | ||||
| -rw-r--r-- | lib/Impure/ImpCore.v | 196 | ||||
| -rw-r--r-- | lib/Impure/ImpExtern.v | 7 | ||||
| -rw-r--r-- | lib/Impure/ImpHCons.v | 199 | ||||
| -rw-r--r-- | lib/Impure/ImpIO.v | 159 | ||||
| -rw-r--r-- | lib/Impure/ImpLoops.v | 123 | ||||
| -rw-r--r-- | lib/Impure/ImpMonads.v | 148 | ||||
| -rw-r--r-- | lib/Impure/ImpPrelude.v | 206 | ||||
| -rw-r--r-- | lib/Impure/LICENSE | 165 | ||||
| -rw-r--r-- | lib/Impure/README.md | 31 | ||||
| -rw-r--r-- | lib/Impure/ocaml/ImpHConsOracles.ml | 72 | ||||
| -rw-r--r-- | lib/Impure/ocaml/ImpHConsOracles.mli | 5 | ||||
| -rw-r--r-- | lib/Impure/ocaml/ImpIOOracles.ml | 142 | ||||
| -rw-r--r-- | lib/Impure/ocaml/ImpIOOracles.mli | 33 | ||||
| -rw-r--r-- | lib/Impure/ocaml/ImpLoopOracles.ml | 78 | ||||
| -rw-r--r-- | lib/Impure/ocaml/ImpLoopOracles.mli | 8 | ||||
| -rw-r--r-- | lib/Integers.v | 213 | ||||
| -rw-r--r-- | lib/IterList.v | 112 | ||||
| -rw-r--r-- | lib/Lattice.v | 110 | ||||
| -rw-r--r-- | lib/Maps.v | 66 | ||||
| -rw-r--r-- | lib/OptionMonad.v | 76 | ||||
| -rw-r--r-- | lib/UnionFind.v | 63 | ||||
| -rw-r--r-- | lib/extra/HashedMap.v | 460 |
28 files changed, 4341 insertions, 19 deletions
diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 045fb03a..19c641e3 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -1136,6 +1136,41 @@ Proof. induction 1; intros. auto. apply IHis_tail. eapply is_tail_cons_left; eauto. Qed. +Lemma is_tail_app A (l1: list A): forall l2, is_tail l2 (l1 ++ l2). +Proof. + induction l1; cbn; auto with coqlib. +Qed. +Hint Resolve is_tail_app: coqlib. + +Lemma is_tail_app_inv A (l1: list A): forall l2 l3, is_tail (l1 ++ l2) l3 -> is_tail l2 l3. +Proof. + induction l1; cbn; auto with coqlib. + intros l2 l3 H; inversion H; eauto with coqlib. +Qed. +Global Hint Resolve is_tail_app_inv: coqlib. + +Lemma is_tail_app_right A (l2 l1: list A): is_tail l1 (l2++l1). +Proof. + intros; eauto with coqlib. +Qed. + +Lemma is_tail_app_def A (l1 l2: list A): + is_tail l1 l2 -> exists l3, l2 = l3 ++ l1. +Proof. + induction 1 as [|x l1 l2]; simpl. + - exists nil; simpl; auto. + - destruct IHis_tail as (l3 & EQ); rewrite EQ. + exists (x::l3); simpl; auto. +Qed. + +Lemma is_tail_bound A (l1 l2: list A): + is_tail l1 l2 -> (length l1 <= length l2)%nat. +Proof. + intros H; destruct (is_tail_app_def H) as (l3 & EQ). + subst; rewrite app_length. + lia. +Qed. + (** [list_forall2 P [x1 ... xN] [y1 ... yM]] holds iff [N = M] and [P xi yi] holds for all [i]. *) @@ -1388,3 +1423,9 @@ Lemma nlist_forall2_imply: Proof. induction 1; simpl; intros; constructor; auto. Qed. + +Lemma if_same : forall {T : Type} (b : bool) (x : T), + (if b then x else x) = x. +Proof. + destruct b; trivial. +Qed. diff --git a/lib/Floats.v b/lib/Floats.v index 43caebb0..9ee5302d 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -17,7 +17,7 @@ (** Formalization of floating-point numbers, using the Flocq library. *) -Require Import Coqlib Zbits Integers. +Require Import Coqlib Zbits Integers Axioms. From Flocq Require Import Binary Bits Core. Require Import IEEE754_extra. Require Import Program. @@ -29,8 +29,69 @@ Open Scope Z_scope. Set Asymmetric Patterns. Definition float := binary64. (**r the type of IEE754 double-precision FP numbers *) + +Definition float_eq: forall (i1 i2: float), {i1=i2} + {i1<>i2}. +Proof. + intros. destruct i1. +(* B754_zero *) + - destruct i2; try (right; discriminate). + destruct (eqb s s0) eqn:BEQ. + + apply eqb_prop in BEQ. subst. left. reflexivity. + + apply eqb_false_iff in BEQ. right. intro. inv H. contradiction. +(* B754_infinity *) + - destruct i2; try (right; discriminate). + destruct (eqb s s0) eqn:BEQ. + + apply eqb_prop in BEQ. subst. left. reflexivity. + + apply eqb_false_iff in BEQ. right. intro. inv H. contradiction. +(* B754_nan *) + - destruct i2; try (right; discriminate). + destruct (eqb s s0) eqn:BEQ. + + generalize (Pos.eq_dec pl pl0). intro. inv H. + ++ left. apply eqb_prop in BEQ. subst. + assert (e = e0) by (apply proof_irr). congruence. + ++ right. intro. inv H. contradiction. + + apply eqb_false_iff in BEQ. right. intro. inv H. contradiction. +(* B754_finite *) + - destruct i2; try (right; discriminate). + destruct (eqb s s0) eqn:BEQ; [apply eqb_prop in BEQ | apply eqb_false_iff in BEQ]. + generalize (Pos.eq_dec m m0). intro. inv H. + generalize (Z.eq_dec e e1). intro. inv H. + 1: { left. assert (e0 = e2) by (apply proof_irr). congruence. } + all: right; intro; inv H; contradiction. +Qed. + Definition float32 := binary32. (**r the type of IEE754 single-precision FP numbers *) +Definition float32_eq: forall (i1 i2: float32), {i1=i2} + {i1<>i2}. +Proof. + intros. destruct i1. +(* B754_zero *) + - destruct i2; try (right; discriminate). + destruct (eqb s s0) eqn:BEQ. + + apply eqb_prop in BEQ. subst. left. reflexivity. + + apply eqb_false_iff in BEQ. right. intro. inv H. contradiction. +(* B754_infinity *) + - destruct i2; try (right; discriminate). + destruct (eqb s s0) eqn:BEQ. + + apply eqb_prop in BEQ. subst. left. reflexivity. + + apply eqb_false_iff in BEQ. right. intro. inv H. contradiction. +(* B754_nan *) + - destruct i2; try (right; discriminate). + destruct (eqb s s0) eqn:BEQ. + + generalize (Pos.eq_dec pl pl0). intro. inv H. + ++ left. apply eqb_prop in BEQ. subst. + assert (e = e0) by (apply proof_irr). congruence. + ++ right. intro. inv H. contradiction. + + apply eqb_false_iff in BEQ. right. intro. inv H. contradiction. +(* B754_finite *) + - destruct i2; try (right; discriminate). + destruct (eqb s s0) eqn:BEQ; [apply eqb_prop in BEQ | apply eqb_false_iff in BEQ]. + generalize (Pos.eq_dec m m0). intro. inv H. + generalize (Z.eq_dec e e1). intro. inv H. + 1: { left. assert (e0 = e2) by (apply proof_irr). congruence. } + all: right; intro; inv H; contradiction. +Qed. + (** Boolean-valued comparisons *) Definition cmp_of_comparison (c: comparison) (x: option Datatypes.comparison) : bool := diff --git a/lib/HashedSet.v b/lib/HashedSet.v new file mode 100644 index 00000000..48798a1b --- /dev/null +++ b/lib/HashedSet.v @@ -0,0 +1,1414 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + +Require Import ZArith. +Require Import Bool. +Require Import List. +Require Coq.Logic.Eqdep_dec. + +(* begin from Maps *) +Fixpoint prev_append (i j: positive) {struct i} : positive := + match i with + | xH => j + | xI i' => prev_append i' (xI j) + | xO i' => prev_append i' (xO j) + end. + +Definition prev (i: positive) : positive := + prev_append i xH. + +Lemma prev_append_prev i j: + prev (prev_append i j) = prev_append j i. +Proof. + revert j. unfold prev. + induction i as [i IH|i IH|]. 3: reflexivity. + intros j. simpl. rewrite IH. reflexivity. + intros j. simpl. rewrite IH. reflexivity. +Qed. + +Lemma prev_involutive i : + prev (prev i) = i. +Proof (prev_append_prev i xH). + +Lemma prev_append_inj i j j' : + prev_append i j = prev_append i j' -> j = j'. +Proof. + revert j j'. + induction i as [i Hi|i Hi|]; intros j j' H; auto; + specialize (Hi _ _ H); congruence. +Qed. + +(* end from Maps *) + +Lemma orb_idem: forall b, orb b b = b. +Proof. + destruct b; reflexivity. +Qed. + +Lemma andb_idem: forall b, andb b b = b. +Proof. + destruct b; reflexivity. +Qed. + +Lemma andb_negb_false: forall b, andb b (negb b) = false. +Proof. + destruct b; reflexivity. +Qed. + +Hint Rewrite orb_false_r andb_false_r andb_true_r orb_true_r orb_idem andb_idem andb_negb_false : pset. + +Module PSet_internals. +Inductive pset : Type := +| Empty : pset +| Node : pset -> bool -> pset -> pset. + +Definition empty := Empty. + +Definition is_empty x := + match x with + | Empty => true + | Node _ _ _ => false + end. + +Fixpoint wf x := + match x with + | Empty => true + | Node b0 f b1 => + (wf b0) && (wf b1) && + ((negb (is_empty b0)) || f || (negb (is_empty b1))) + end. + +Definition iswf x := (wf x)=true. + +Lemma empty_wf : iswf empty. +Proof. + reflexivity. +Qed. + +Definition pset_eq : + forall s s': pset, { s=s' } + { s <> s' }. +Proof. + induction s; destruct s'; repeat decide equality. +Qed. + +Fixpoint contains (s : pset) (i : positive) {struct i} : bool := + match s with + | Empty => false + | Node b0 f b1 => + match i with + | xH => f + | xO ii => contains b0 ii + | xI ii => contains b1 ii + end + end. + +Lemma gempty : + forall i : positive, + contains Empty i = false. +Proof. + destruct i; simpl; reflexivity. +Qed. + +Global Hint Resolve gempty : pset. +Hint Rewrite gempty : pset. + +Definition node (b0 : pset) (f : bool) (b1 : pset) : pset := + match b0, f, b1 with + | Empty, false, Empty => Empty + | _, _, _ => Node b0 f b1 + end. + +Lemma wf_node : + forall b0 f b1, + iswf b0 -> iswf b1 -> iswf (node b0 f b1). +Proof. + destruct b0; destruct f; destruct b1; simpl. + all: unfold iswf; simpl; intros; trivial. + all: autorewrite with pset; trivial. + all: rewrite H. + all: rewrite H0. + all: reflexivity. +Qed. + +Global Hint Resolve wf_node: pset. + +Lemma gnode : + forall b0 f b1 i, + contains (node b0 f b1) i = + contains (Node b0 f b1) i. +Proof. + destruct b0; simpl; trivial. + destruct f; simpl; trivial. + destruct b1; simpl; trivial. + intro. + rewrite gempty. + destruct i; simpl; trivial. + all: symmetry; apply gempty. +Qed. + +Hint Rewrite gnode : pset. + +Fixpoint add (i : positive) (s : pset) {struct i} : pset := + match s with + | Empty => + match i with + | xH => Node Empty true Empty + | xO ii => Node (add ii Empty) false Empty + | xI ii => Node Empty false (add ii Empty) + end + | Node b0 f b1 => + match i with + | xH => Node b0 true b1 + | xO ii => Node (add ii b0) f b1 + | xI ii => Node b0 f (add ii b1) + end + end. + +Lemma add_nonempty: + forall i s, is_empty (add i s) = false. +Proof. + induction i; destruct s; simpl; trivial. +Qed. + +Hint Rewrite add_nonempty : pset. +Global Hint Resolve add_nonempty : pset. + +Lemma wf_add: + forall i s, (iswf s) -> (iswf (add i s)). +Proof. + induction i; destruct s; simpl; trivial. + all: unfold iswf in *; simpl. + all: autorewrite with pset; simpl; trivial. + 1,3: auto with pset. + all: intro Z. + all: repeat rewrite andb_true_iff in Z. + all: intuition. +Qed. + +Global Hint Resolve wf_add : pset. + +Theorem gadds : + forall i : positive, + forall s : pset, + contains (add i s) i = true. +Proof. + induction i; destruct s; simpl; auto. +Qed. + +Global Hint Resolve gadds : pset. +Hint Rewrite gadds : pset. + +Theorem gaddo : + forall i j : positive, + forall s : pset, + i <> j -> + contains (add i s) j = contains s j. +Proof. + induction i; destruct j; destruct s; simpl; intro; auto with pset. + 5, 6: congruence. + all: rewrite IHi by congruence. + all: trivial. + all: apply gempty. +Qed. + +Global Hint Resolve gaddo : pset. + +Fixpoint remove (i : positive) (s : pset) { struct i } : pset := + match i with + | xH => + match s with + | Empty => Empty + | Node b0 f b1 => node b0 false b1 + end + | xO ii => + match s with + | Empty => Empty + | Node b0 f b1 => node (remove ii b0) f b1 + end + | xI ii => + match s with + | Empty => Empty + | Node b0 f b1 => node b0 f (remove ii b1) + end + end. + +Lemma wf_remove : + forall i s, (iswf s) -> (iswf (remove i s)). +Proof. + induction i; destruct s; simpl; trivial. + all: unfold iswf in *; simpl. + all: intro Z. + all: repeat rewrite andb_true_iff in Z. + all: apply wf_node. + all: intuition. + all: apply IHi. + all: assumption. +Qed. + + +Fixpoint remove_noncanon (i : positive) (s : pset) { struct i } : pset := + match i with + | xH => + match s with + | Empty => Empty + | Node b0 f b1 => Node b0 false b1 + end + | xO ii => + match s with + | Empty => Empty + | Node b0 f b1 => Node (remove_noncanon ii b0) f b1 + end + | xI ii => + match s with + | Empty => Empty + | Node b0 f b1 => Node b0 f (remove_noncanon ii b1) + end + end. + +Lemma remove_noncanon_same: + forall i j s, (contains (remove i s) j) = (contains (remove_noncanon i s) j). +Proof. + induction i; destruct s; simpl; trivial. + all: rewrite gnode. + 3: reflexivity. + all: destruct j; simpl; trivial. +Qed. + +Lemma remove_empty : + forall i, remove i Empty = Empty. +Proof. + induction i; simpl; trivial. +Qed. + +Hint Rewrite remove_empty : pset. +Global Hint Resolve remove_empty : pset. + +Lemma gremove_noncanon_s : + forall i : positive, + forall s : pset, + contains (remove_noncanon i s) i = false. +Proof. + induction i; destruct s; simpl; trivial. +Qed. + +Theorem gremoves : + forall i : positive, + forall s : pset, + contains (remove i s) i = false. +Proof. + intros. + rewrite remove_noncanon_same. + apply gremove_noncanon_s. +Qed. + +Global Hint Resolve gremoves : pset. +Hint Rewrite gremoves : pset. + +Lemma gremove_noncanon_o : + forall i j : positive, + forall s : pset, + i<>j -> + contains (remove_noncanon i s) j = contains s j. +Proof. + induction i; destruct j; destruct s; simpl; intro; trivial. + 1, 2: rewrite IHi by congruence. + 1, 2: reflexivity. + congruence. +Qed. + +Theorem gremoveo : + forall i j : positive, + forall s : pset, + i<>j -> + contains (remove i s) j = contains s j. +Proof. + intros. + rewrite remove_noncanon_same. + apply gremove_noncanon_o. + assumption. +Qed. + +Global Hint Resolve gremoveo : pset. + +Fixpoint union_nonopt (s s' : pset) : pset := + match s, s' with + | Empty, _ => s' + | _, Empty => s + | (Node b0 f b1), (Node b0' f' b1') => + Node (union_nonopt b0 b0') (orb f f') (union_nonopt b1 b1') + end. + +Theorem gunion_nonopt: + forall s s' : pset, + forall j : positive, + (contains (union_nonopt s s')) j = orb (contains s j) (contains s' j). +Proof. + induction s; destruct s'; intro; simpl; autorewrite with pset; simpl; trivial. + destruct j; simpl; trivial. +Qed. + + +Fixpoint union (s s' : pset) : pset := + if pset_eq s s' then s else + match s, s' with + | Empty, _ => s' + | _, Empty => s + | (Node b0 f b1), (Node b0' f' b1') => + Node (union b0 b0') (orb f f') (union b1 b1') + end. + +Lemma union_nonempty1: + forall s s', + (is_empty s) = false -> is_empty (union s s')= false. +Proof. + induction s; destruct s'; simpl; try discriminate. + all: destruct pset_eq; simpl; trivial. +Qed. + +Lemma union_nonempty2: + forall s s', + (is_empty s') = false -> is_empty (union s s')= false. +Proof. + induction s; destruct s'; simpl; try discriminate. + all: destruct pset_eq; simpl; trivial; discriminate. +Qed. + +Global Hint Resolve union_nonempty1 union_nonempty2 : pset. + +Lemma wf_union : + forall s s', (iswf s) -> (iswf s') -> (iswf (union s s')). +Proof. + induction s; destruct s'; intros; simpl. + all: destruct pset_eq; trivial. + unfold iswf in *. simpl in *. + repeat rewrite andb_true_iff in H. + repeat rewrite andb_true_iff in H0. + rewrite IHs1. + rewrite IHs2. + simpl. + all: intuition. + repeat rewrite orb_true_iff in H2, H3. + repeat rewrite negb_true_iff in H2, H3. + repeat rewrite orb_true_iff. + repeat rewrite negb_true_iff. + intuition auto with pset. +Qed. + +Global Hint Resolve wf_union : pset. + +Theorem gunion: + forall s s' : pset, + forall j : positive, + (contains (union s s')) j = orb (contains s j) (contains s' j). +Proof. + induction s; destruct s'; intro; simpl. + all: destruct pset_eq as [EQ | NEQ]; try congruence. + all: autorewrite with pset; simpl; trivial. + - rewrite <- EQ. + symmetry. + apply orb_idem. + - destruct j; simpl; trivial. +Qed. + +Fixpoint inter_noncanon (s s' : pset) : pset := + if pset_eq s s' then s else + match s, s' with + | Empty, _ | _, Empty => Empty + | (Node b0 f b1), (Node b0' f' b1') => + Node (inter_noncanon b0 b0') (andb f f') (inter_noncanon b1 b1') + end. + +Lemma ginter_noncanon: + forall s s' : pset, + forall j : positive, + (contains (inter_noncanon s s')) j = andb (contains s j) (contains s' j). +Proof. + induction s; destruct s'; intro; simpl. + all: destruct pset_eq as [EQ | NEQ]; try congruence. + all: autorewrite with pset; simpl; trivial. + - rewrite <- EQ. + symmetry. + apply andb_idem. + - destruct j; simpl; trivial. +Qed. + +Fixpoint inter (s s' : pset) : pset := + if pset_eq s s' then s else + match s, s' with + | Empty, _ | _, Empty => Empty + | (Node b0 f b1), (Node b0' f' b1') => + node (inter b0 b0') (andb f f') (inter b1 b1') + end. + +Lemma wf_inter : + forall s s', (iswf s) -> (iswf s') -> (iswf (inter s s')). +Proof. + induction s; destruct s'; intros; simpl. + all: destruct pset_eq; trivial. + unfold iswf in H, H0. + simpl in H, H0. + repeat rewrite andb_true_iff in H. + repeat rewrite andb_true_iff in H0. + fold (iswf s1) in *. + fold (iswf s2) in *. + intuition. +Qed. + +Global Hint Resolve wf_inter : pset. + +Lemma inter_noncanon_same: + forall s s' j, (contains (inter s s') j) = (contains (inter_noncanon s s') j). +Proof. + induction s; destruct s'; simpl; trivial. + destruct pset_eq; trivial. + destruct j; rewrite gnode; simpl; auto. +Qed. + +Theorem ginter: + forall s s' : pset, + forall j : positive, + (contains (inter s s')) j = andb (contains s j) (contains s' j). +Proof. + intros. + rewrite inter_noncanon_same. + apply ginter_noncanon. +Qed. + +Global Hint Resolve ginter gunion : pset. +Hint Rewrite ginter gunion : pset. + +Fixpoint subtract_noncanon (s s' : pset) : pset := + if pset_eq s s' then Empty else + match s, s' with + | Empty, _ => Empty + | _, Empty => s + | (Node b0 f b1), (Node b0' f' b1') => + Node (subtract_noncanon b0 b0') (andb f (negb f')) (subtract_noncanon b1 b1') + end. + +Lemma gsubtract_noncanon: + forall s s' : pset, + forall j : positive, + (contains (subtract_noncanon s s')) j = andb (contains s j) (negb (contains s' j)). +Proof. + induction s; destruct s'; intro; simpl. + all: destruct pset_eq as [EQ | NEQ]; try congruence. + all: autorewrite with pset; simpl; trivial. + - rewrite <- EQ. + symmetry. + apply andb_negb_false. + - destruct j; simpl; trivial. +Qed. + +Fixpoint subtract (s s' : pset) : pset := + if pset_eq s s' then Empty else + match s, s' with + | Empty, _ => Empty + | _, Empty => s + | (Node b0 f b1), (Node b0' f' b1') => + node (subtract b0 b0') (andb f (negb f')) (subtract b1 b1') + end. + +Lemma wf_subtract : + forall s s', (iswf s) -> (iswf s') -> (iswf (subtract s s')). +Proof. + induction s; destruct s'; intros; simpl. + all: destruct pset_eq; trivial. + reflexivity. + + unfold iswf in H, H0. + simpl in H, H0. + + repeat rewrite andb_true_iff in H. + repeat rewrite andb_true_iff in H0. + fold (iswf s1) in *. + fold (iswf s2) in *. + intuition. +Qed. + +Global Hint Resolve wf_subtract : pset. + +Lemma subtract_noncanon_same: + forall s s' j, (contains (subtract s s') j) = (contains (subtract_noncanon s s') j). +Proof. + induction s; destruct s'; simpl; trivial. + destruct pset_eq; trivial. + destruct j; rewrite gnode; simpl; auto. +Qed. + +Theorem gsubtract: + forall s s' : pset, + forall j : positive, + (contains (subtract s s')) j = andb (contains s j) (negb (contains s' j)). +Proof. + intros. + rewrite subtract_noncanon_same. + apply gsubtract_noncanon. +Qed. + +Global Hint Resolve gsubtract : pset. +Hint Rewrite gsubtract : pset. + +Lemma wf_is_nonempty : + forall s, iswf s -> is_empty s = false -> exists i, contains s i = true. +Proof. + induction s; simpl; trivial. + discriminate. + intro WF. + unfold iswf in WF. + simpl in WF. + repeat rewrite andb_true_iff in WF. + repeat rewrite orb_true_iff in WF. + repeat rewrite negb_true_iff in WF. + fold (iswf s1) in WF. + fold (iswf s2) in WF. + intuition. + - destruct H5 as [i K]. + exists (xO i). + simpl. + assumption. + - exists xH. + simpl. + assumption. + - destruct H5 as [i K]. + exists (xI i). + simpl. + assumption. +Qed. + +Global Hint Resolve wf_is_nonempty : pset. + +Lemma wf_is_empty1 : + forall s, iswf s -> (forall i, (contains s i) = false) -> is_empty s = true. +Proof. + induction s; trivial. + intro WF. + unfold iswf in WF. + simpl in WF. + repeat rewrite andb_true_iff in WF. + fold (iswf s1) in WF. + fold (iswf s2) in WF. + intro ALL. + intuition. + exfalso. + repeat rewrite orb_true_iff in H0. + repeat rewrite negb_true_iff in H0. + intuition. + - rewrite H in H0. discriminate. + intro i. + specialize ALL with (xO i). + simpl in ALL. + assumption. + - specialize ALL with xH. + simpl in ALL. + congruence. + - rewrite H3 in H4. discriminate. + intro i. + specialize ALL with (xI i). + simpl in ALL. + assumption. +Qed. + +Global Hint Resolve wf_is_empty1 : pset. + +Lemma wf_eq : + forall s s', iswf s -> iswf s' -> s <> s' -> + exists i, (contains s i) <> (contains s' i). +Proof. + induction s; destruct s'; intros WF WF' DIFF; simpl. + - congruence. + - assert (exists i, (contains (Node s'1 b s'2) i)= true) as K by auto with pset. + destruct K as [i Z]. + exists i. + rewrite Z. + rewrite gempty. + discriminate. + - assert (exists i, (contains (Node s1 b s2) i)= true) as K by auto with pset. + destruct K as [i Z]. + exists i. + rewrite Z. + rewrite gempty. + discriminate. + - destruct (pset_eq s1 s'1). + + subst s'1. + destruct (pset_eq s2 s'2). + * subst s'2. + exists xH. + simpl. + congruence. + * specialize IHs2 with s'2. + unfold iswf in WF. + simpl in WF. + repeat rewrite andb_true_iff in WF. + fold (iswf s1) in WF. + fold (iswf s2) in WF. + unfold iswf in WF'. + simpl in WF'. + repeat rewrite andb_true_iff in WF'. + fold (iswf s'2) in WF'. + intuition. + destruct H1 as [i K]. + exists (xI i). + simpl. + assumption. + + specialize IHs1 with s'1. + unfold iswf in WF. + simpl in WF. + repeat rewrite andb_true_iff in WF. + fold (iswf s1) in WF. + fold (iswf s2) in WF. + unfold iswf in WF'. + simpl in WF'. + repeat rewrite andb_true_iff in WF'. + fold (iswf s'1) in WF'. + fold (iswf s'2) in WF'. + intuition. + destruct H1 as [i K]. + exists (xO i). + simpl. + assumption. +Qed. + +Theorem eq_correct: + forall s s', + (iswf s) -> (iswf s') -> + (forall i, (contains s i) = (contains s' i)) <-> s = s'. +Proof. + intros s s' WF WF'. + split. + { + intro ALL. + destruct (pset_eq s s') as [ | INEQ]; trivial. + exfalso. + destruct (wf_eq s s' WF WF' INEQ) as [i K]. + specialize ALL with i. + congruence. + } + intro EQ. + subst s'. + trivial. +Qed. + +Lemma wf_irrelevant: + forall s, + forall WF WF' : iswf s, WF = WF'. +Proof. + unfold iswf. + intros. + apply Coq.Logic.Eqdep_dec.eq_proofs_unicity_on. + decide equality. +Qed. + +Fixpoint xelements (s : pset) (i : positive) + (k: list positive) {struct s} + : list positive := + match s with + | Empty => k + | Node b0 false b1 => + xelements b0 (xO i) (xelements b1 (xI i) k) + | Node b0 true b1 => + xelements b0 (xO i) ((prev i) :: xelements b1 (xI i) k) + end. + +Definition elements (m : pset) := xelements m xH nil. + + Remark xelements_append: + forall (m: pset) i k1 k2, + xelements m i (k1 ++ k2) = xelements m i k1 ++ k2. + Proof. + induction m; intros; simpl. + - auto. + - destruct b; rewrite IHm2; rewrite <- IHm1; auto. + Qed. + + Remark xelements_empty: + forall i, xelements Empty i nil = nil. + Proof. + intros; reflexivity. + Qed. + + Remark xelements_node: + forall (m1: pset) o (m2: pset) i, + xelements (Node m1 o m2) i nil = + xelements m1 (xO i) nil + ++ (if o then (prev i) :: nil else nil) + ++ xelements m2 (xI i) nil. + Proof. + intros. simpl. destruct o; simpl; + rewrite <- xelements_append; trivial. + Qed. + + Lemma xelements_incl: + forall (m: pset) (i : positive) k x, + In x k -> In x (xelements m i k). + Proof. + induction m; intros; simpl. + auto. + destruct b. + apply IHm1. simpl; right; auto. + auto. + Qed. + + Lemma xelements_correct: + forall (m: pset) (i j : positive) k, + contains m i=true -> In (prev (prev_append i j)) (xelements m j k). + Proof. + induction m; intros; simpl. + - rewrite gempty in H. discriminate. + - destruct b; destruct i; simpl; simpl in H; auto. + + apply xelements_incl. simpl. + right. auto. + + apply xelements_incl. simpl. + left. trivial. + + apply xelements_incl. auto. + + discriminate. + Qed. + + Theorem elements_correct: + forall (m: pset) (i: positive), + contains m i = true -> In i (elements m). + Proof. + intros m i H. + generalize (xelements_correct m i xH nil H). rewrite prev_append_prev. exact id. + Qed. + + Lemma in_xelements: + forall (m: pset) (i k: positive), + In k (xelements m i nil) -> + exists j, k = prev (prev_append j i) /\ contains m j = true. + Proof. + induction m; intros. + - rewrite xelements_empty in H. contradiction. + - rewrite xelements_node in H. rewrite ! in_app_iff in H. destruct H as [P | [P | P]]. + + specialize IHm1 with (k := k) (i := xO i). + intuition. + destruct H as [j [Q R]]. + exists (xO j). + auto. + + destruct b; simpl in P; intuition auto. subst k. exists xH; auto. + + specialize IHm2 with (k := k) (i := xI i). + intuition. + destruct H as [j [Q R]]. + exists (xI j). + auto. + Qed. + + Theorem elements_complete: + forall (m: pset) (i: positive), + In i (elements m) -> contains m i = true. + Proof. + unfold elements. intros m i H. + destruct (in_xelements m 1 i H) as [j [P Q]]. + rewrite prev_append_prev in P. change i with (prev_append 1 i) in P. + replace j with i in * by (apply prev_append_inj; auto). + assumption. + Qed. + + + Fixpoint xfold {B: Type} (f: B -> positive -> B) + (i: positive) (m: pset) (v: B) {struct m} : B := + match m with + | Empty => v + | Node l false r => + let v1 := xfold f (xO i) l v in + xfold f (xI i) r v1 + | Node l true r => + let v1 := xfold f (xO i) l v in + let v2 := f v1 (prev i) in + xfold f (xI i) r v2 + end. + + Definition fold {B : Type} (f: B -> positive -> B) (m: pset) (v: B) := + xfold f xH m v. + + + Lemma xfold_xelements: + forall {B: Type} (f: B -> positive -> B) m i v l, + List.fold_left f l (xfold f i m v) = + List.fold_left f (xelements m i l) v. + Proof. + induction m; intros; simpl; trivial. + destruct b; simpl. + all: rewrite <- IHm1; simpl; rewrite <- IHm2; trivial. + Qed. + + Theorem fold_spec: + forall {B: Type} (f: B -> positive -> B) (v: B) (m: pset), + fold f m v = + List.fold_left f (elements m) v. + Proof. + intros. unfold fold, elements. rewrite <- xfold_xelements. auto. + Qed. + + Fixpoint is_subset (s s' : pset) {struct s} := + if pset_eq s s' then true else + match s, s' with + | Empty, _ => true + | _, Empty => false + | (Node b0 f b1), (Node b0' f' b1') => + ((negb f) || f') && + (is_subset b0 b0') && + (is_subset b1 b1') + end. + + Theorem is_subset_spec1: + forall s s', + is_subset s s' = true -> + (forall i, contains s i = true -> contains s' i = true). + Proof. + induction s; destruct s'; simpl; intros; trivial. + all: destruct pset_eq. + all: try discriminate. + all: try rewrite gempty in *. + all: try discriminate. + { congruence. + } + repeat rewrite andb_true_iff in H. + repeat rewrite orb_true_iff in H. + repeat rewrite negb_true_iff in H. + specialize IHs1 with (s' := s'1). + specialize IHs2 with (s' := s'2). + intuition. + - destruct i; simpl in *; auto. congruence. + - destruct i; simpl in *; auto. + Qed. + + Theorem is_subset_spec2: + forall s s', + iswf s -> + (forall i, contains s i = true -> contains s' i = true) -> + is_subset s s' = true. + Proof. + induction s; destruct s'; simpl. + all: intro WF. + all: unfold iswf in WF. + all: simpl in WF. + all: repeat rewrite andb_true_iff in WF. + all: destruct pset_eq; trivial. + all: fold (iswf s1) in WF. + all: fold (iswf s2) in WF. + - repeat rewrite orb_true_iff in WF. + repeat rewrite negb_true_iff in WF. + intuition. + + destruct (wf_is_nonempty s1 H2 H1) as [i K]. + specialize H with (xO i). + simpl in H. + auto. + + specialize H with xH. + simpl in H. + auto. + + destruct (wf_is_nonempty s2 H3 H0) as [i K]. + specialize H with (xI i). + simpl in H. + auto. + - intro CONTAINS. + repeat rewrite andb_true_iff. + specialize IHs1 with (s' := s'1). + specialize IHs2 with (s' := s'2). + intuition. + + specialize CONTAINS with xH. + simpl in CONTAINS. + destruct b; destruct b0; intuition congruence. + + apply H. + intros. + specialize CONTAINS with (xO i). + simpl in CONTAINS. + auto. + + apply H3. + intros. + specialize CONTAINS with (xI i). + simpl in CONTAINS. + auto. + Qed. + + Fixpoint xfilter (fn : positive -> bool) + (s : pset) (i : positive) {struct s} : pset := + match s with + | Empty => Empty + | Node b0 f b1 => + node (xfilter fn b0 (xO i)) + (f && (fn (prev i))) + (xfilter fn b1 (xI i)) + end. + + Lemma gxfilter: + forall fn s j i, + contains (xfilter fn s i) j = + contains s j && + (fn (prev (prev_append j i))). + Proof. + induction s; simpl; intros; trivial. + { + rewrite gempty. + trivial. + } + rewrite gnode. + destruct j; simpl; auto. + Qed. + + Definition filter (fn : positive -> bool) m := xfilter fn m xH. + + Lemma gfilter: + forall fn s j, + contains (filter fn s) j = + contains s j && (fn j). + Proof. + intros. + unfold filter. + rewrite gxfilter. + rewrite prev_append_prev. + reflexivity. + Qed. + + Lemma wf_xfilter: + forall fn s j, + iswf s -> iswf (xfilter fn s j). + Proof. + induction s; intros; trivial. + simpl. + unfold iswf in H. + simpl in H. + repeat rewrite andb_true_iff in H. + fold (iswf s1) in H. + fold (iswf s2) in H. + intuition. + Qed. + + Lemma wf_filter: + forall fn s, + iswf s -> iswf (filter fn s). + Proof. + intros. + apply wf_xfilter; auto. + Qed. +End PSet_internals. + +Module Type POSITIVE_SET. +Parameter t : Type. +Parameter empty : t. + +Parameter contains: t -> positive -> bool. + +Axiom gempty : + forall i : positive, + contains empty i = false. + +Parameter add : positive -> t -> t. + +Axiom gaddo : + forall i j : positive, + forall s : t, + i <> j -> + contains (add i s) j = contains s j. + +Axiom gadds : + forall i : positive, + forall s : t, + contains (add i s) i = true. + +Parameter remove : positive -> t -> t. + +Axiom gremoves : + forall i : positive, + forall s : t, + contains (remove i s) i = false. + +Axiom gremoveo : + forall i j : positive, + forall s : t, + i<>j -> + contains (remove i s) j = contains s j. + +Parameter union : t -> t -> t. + +Axiom gunion: + forall s s' : t, + forall j : positive, + (contains (union s s')) j = orb (contains s j) (contains s' j). + +Parameter inter : t -> t -> t. + +Axiom ginter: + forall s s' : t, + forall j : positive, + (contains (inter s s')) j = andb (contains s j) (contains s' j). + +Parameter subtract : t -> t -> t. + +Axiom gsubtract: + forall s s' : t, + forall j : positive, + (contains (subtract s s')) j = andb (contains s j) (negb (contains s' j)). + +Axiom uneq_exists : + forall s s', s <> s' -> + exists i, (contains s i) <> (contains s' i). + +Parameter eq: + forall s s' : t, {s = s'} + {s <> s'}. + +Axiom eq_spec : + forall s s', + (forall i, (contains s i) = (contains s' i)) <-> s = s'. + +Parameter elements : t -> list positive. + +Axiom elements_correct: + forall (m: t) (i: positive), + contains m i = true -> In i (elements m). + +Axiom elements_complete: + forall (m: t) (i: positive), + In i (elements m) -> contains m i = true. + +Axiom elements_spec: + forall (m: t) (i: positive), + In i (elements m) <-> contains m i = true. + +Parameter fold: + forall {B : Type}, + (B -> positive -> B) -> t -> B -> B. + +Axiom fold_spec: + forall {B: Type} (f: B -> positive -> B) (v: B) (m: t), + fold f m v = + List.fold_left f (elements m) v. + +Parameter is_subset : t -> t -> bool. + +Axiom is_subset_spec1: + forall s s', + is_subset s s' = true -> + (forall i, contains s i = true -> contains s' i = true). + +Axiom is_subset_spec2: + forall s s', + (forall i, contains s i = true -> contains s' i = true) -> + is_subset s s' = true. + +Axiom is_subset_spec: + forall s s', + is_subset s s' = true <-> + (forall i, contains s i = true -> contains s' i = true). + +Parameter filter: (positive -> bool) -> t -> t. + +Axiom gfilter: + forall fn s j, + contains (filter fn s) j = + contains s j && (fn j). + +End POSITIVE_SET. + +Module PSet : POSITIVE_SET. + +Record pset : Type := mkpset +{ + pset_x : PSet_internals.pset ; + pset_wf : PSet_internals.wf pset_x = true +}. + +Definition t := pset. + +Program Definition empty : t := mkpset PSet_internals.empty _. + +Definition contains (s : t) (i : positive) := + PSet_internals.contains (pset_x s) i. + +Theorem gempty : + forall i : positive, + contains empty i = false. +Proof. + intro. + unfold empty, contains. + simpl. + auto with pset. +Qed. + +Program Definition add (i : positive) (s : t) := + mkpset (PSet_internals.add i (pset_x s)) _. +Obligation 1. + destruct s. + apply PSet_internals.wf_add. + simpl. + assumption. +Qed. + +Theorem gaddo : + forall i j : positive, + forall s : t, + i <> j -> + contains (add i s) j = contains s j. +Proof. + intros. + unfold contains. + simpl. + auto with pset. +Qed. + +Theorem gadds : + forall i : positive, + forall s : pset, + contains (add i s) i = true. +Proof. + intros. + unfold contains. + simpl. + auto with pset. +Qed. + +Program Definition remove (i : positive) (s : t) := + mkpset (PSet_internals.remove i (pset_x s)) _. +Obligation 1. + destruct s. + apply PSet_internals.wf_remove. + simpl. + assumption. +Qed. + +Theorem gremoves : + forall i : positive, + forall s : pset, + contains (remove i s) i = false. +Proof. + intros. + unfold contains. + simpl. + auto with pset. +Qed. + +Theorem gremoveo : + forall i j : positive, + forall s : pset, + i<>j -> + contains (remove i s) j = contains s j. +Proof. + intros. + unfold contains. + simpl. + auto with pset. +Qed. + +Program Definition union (s s' : t) := + mkpset (PSet_internals.union (pset_x s) (pset_x s')) _. +Obligation 1. + destruct s; destruct s'. + apply PSet_internals.wf_union; simpl; assumption. +Qed. + +Theorem gunion: + forall s s' : pset, + forall j : positive, + (contains (union s s')) j = orb (contains s j) (contains s' j). +Proof. + intros. + unfold contains. + simpl. + auto with pset. +Qed. + +Program Definition inter (s s' : t) := + mkpset (PSet_internals.inter (pset_x s) (pset_x s')) _. +Obligation 1. + destruct s; destruct s'. + apply PSet_internals.wf_inter; simpl; assumption. +Qed. + +Theorem ginter: + forall s s' : pset, + forall j : positive, + (contains (inter s s')) j = andb (contains s j) (contains s' j). +Proof. + intros. + unfold contains. + simpl. + auto with pset. +Qed. + +Program Definition subtract (s s' : t) := + mkpset (PSet_internals.subtract (pset_x s) (pset_x s')) _. +Obligation 1. + destruct s; destruct s'. + apply PSet_internals.wf_subtract; simpl; assumption. +Qed. + +Theorem gsubtract: + forall s s' : pset, + forall j : positive, + (contains (subtract s s')) j = andb (contains s j) (negb (contains s' j)). +Proof. + intros. + unfold contains. + simpl. + auto with pset. +Qed. + +Theorem uneq_exists : + forall s s', s <> s' -> + exists i, (contains s i) <> (contains s' i). +Proof. + destruct s as [s WF]; destruct s' as [s' WF']; simpl. + intro UNEQ. + destruct (PSet_internals.pset_eq s s'). + { subst s'. + pose proof (PSet_internals.wf_irrelevant s WF WF'). + subst WF'. + congruence. + } + unfold contains; simpl. + apply PSet_internals.wf_eq; trivial. +Qed. + +Definition eq: + forall s s' : t, {s = s'} + {s <> s'}. +Proof. + destruct s as [s WF]. + destruct s' as [s' WF']. + destruct (PSet_internals.pset_eq s s'); simpl. + { + subst s'. + left. + pose proof (PSet_internals.wf_irrelevant s WF WF'). + subst WF'. + reflexivity. + } + right. + congruence. +Qed. + +Theorem eq_spec : + forall s s', + (forall i, (contains s i) = (contains s' i)) <-> s = s'. +Proof. + intros. + split; intro K. + 2: subst s'; reflexivity. + destruct s as [s WF]. + destruct s' as [s' WF']. + unfold contains in K. + simpl in K. + fold (PSet_internals.iswf s) in WF. + fold (PSet_internals.iswf s') in WF'. + assert (s = s'). + { + apply PSet_internals.eq_correct; assumption. + } + subst s'. + pose proof (PSet_internals.wf_irrelevant s WF WF'). + subst WF'. + reflexivity. +Qed. + + +Definition elements (m : t) := PSet_internals.elements (pset_x m). + + +Theorem elements_correct: + forall (m: pset) (i: positive), + contains m i = true -> In i (elements m). +Proof. + destruct m; unfold elements, contains; simpl. + apply PSet_internals.elements_correct. +Qed. + +Theorem elements_complete: + forall (m: pset) (i: positive), + In i (elements m) -> contains m i = true. +Proof. + destruct m; unfold elements, contains; simpl. + apply PSet_internals.elements_complete. +Qed. + + +Theorem elements_spec: + forall (m: pset) (i: positive), + In i (elements m) <-> contains m i = true. +Proof. + intros. split. + - apply elements_complete. + - apply elements_correct. +Qed. + +Definition fold {B : Type} (f : B -> positive -> B) (m : t) (v : B) : B := + PSet_internals.fold f (pset_x m) v. + +Theorem fold_spec: + forall {B: Type} (f: B -> positive -> B) (v: B) (m: pset), + fold f m v = + List.fold_left f (elements m) v. +Proof. + destruct m; unfold fold, elements; simpl. + apply PSet_internals.fold_spec. +Qed. + +Definition is_subset (s s' : t) := PSet_internals.is_subset (pset_x s) (pset_x s'). + +Theorem is_subset_spec1: + forall s s', + is_subset s s' = true -> + (forall i, contains s i = true -> contains s' i = true). +Proof. + unfold is_subset, contains. + intros s s' H. + apply PSet_internals.is_subset_spec1. + assumption. +Qed. + +Theorem is_subset_spec2: + forall s s', + (forall i, contains s i = true -> contains s' i = true) -> + is_subset s s' = true. +Proof. + destruct s; destruct s'; + unfold is_subset, contains; + intros. + apply PSet_internals.is_subset_spec2. + all: simpl. + all: assumption. +Qed. + +Global Hint Resolve is_subset_spec1 is_subset_spec2 : pset. + +Theorem is_subset_spec: + forall s s', + is_subset s s' = true <-> + (forall i, contains s i = true -> contains s' i = true). +Proof. + intros. + split; + eauto with pset. +Qed. + +Program Definition filter (fn : positive -> bool) (m : t) : t := + (mkpset (PSet_internals.filter fn (pset_x m)) _). +Obligation 1. + apply PSet_internals.wf_filter. + unfold PSet_internals.iswf. + destruct m. + assumption. +Qed. + +Theorem gfilter: + forall fn s j, + contains (filter fn s) j = + contains s j && (fn j). +Proof. + unfold contains, filter. + simpl. + intros. + apply PSet_internals.gfilter. +Qed. +End PSet. + +Global Hint Resolve PSet.gaddo PSet.gadds PSet.gremoveo PSet.gremoves PSet.gunion PSet.ginter PSet.gsubtract PSet.gfilter PSet.is_subset_spec1 PSet.is_subset_spec2 : pset. + +Hint Rewrite PSet.gadds PSet.gremoves PSet.gunion PSet.ginter PSet.gsubtract PSet.gfilter : pset. diff --git a/lib/HashedSetaux.ml b/lib/HashedSetaux.ml new file mode 100644 index 00000000..501475d6 --- /dev/null +++ b/lib/HashedSetaux.ml @@ -0,0 +1,67 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + +type uid = int + +let uid_base = min_int +let next_uid = ref (uid_base+1) + +let incr_uid () = + let r = !next_uid in + if r = max_int + then failwith "HashedSet: no more uid" + else next_uid := succ r;; + +let cur_uid () = !next_uid;; + +type pset = + | Empty + | Node of uid * pset * bool * pset;; + +let get_uid = function + | Empty -> uid_base + | Node(uid, _, _, _) -> uid;; + +module HashedPSet = + struct + type t = pset + + let hash = function + | Empty -> 0 + | Node(_, b0, f, b1) -> Hashtbl.hash (get_uid b0, f, get_uid b1);; + + let equal x x' = match x, x' with + | Empty, Empty -> true + | Node(_, b0, f, b1), Node(_, b0', f', b1') -> + b0 == b0' && f == f' && b1 == b1' + | _, _ -> false + end;; + +module PSetHash = Weak.Make(HashedPSet);; + +let htable = PSetHash.create 1000;; + +let qnode b0 f b1 = + let x = Node(cur_uid(), b0, f, b1) in + match PSetHash.find_opt htable x with + | None -> PSetHash.add htable x; incr_uid(); x + | Some y -> y;; + +let node (b0, f, b1) = qnode b0 f b1;; + +let empty = Empty;; + +let pset_match empty_case node_case = function + | Empty -> empty_case () + | Node(_, b0, f, b1) -> node_case b0 f b1;; + +let eq (x : pset) (y : pset) = (x==y);; diff --git a/lib/HashedSetaux.mli b/lib/HashedSetaux.mli new file mode 100644 index 00000000..e3426eb4 --- /dev/null +++ b/lib/HashedSetaux.mli @@ -0,0 +1,18 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + +type pset +val qnode : pset -> bool -> pset -> pset +val node : pset * bool * pset -> pset +val empty : pset +val pset_match : (unit -> 'a) -> (pset -> bool -> pset -> 'a) -> pset -> 'a +val eq : pset -> pset -> bool diff --git a/lib/Impure/ImpConfig.v b/lib/Impure/ImpConfig.v new file mode 100644 index 00000000..dd9785b5 --- /dev/null +++ b/lib/Impure/ImpConfig.v @@ -0,0 +1,85 @@ +(** Impure Config for UNTRUSTED backend !!! *) + +Require Import ImpMonads. +Require Extraction. +(** Pure computations (used for extraction !) + +We keep module [Impure] opaque in order to check that Coq proof do not depend on +the implementation of [Impure]. + +*) + +Module Type ImpureView. + + Include MayReturnMonad. + +(* WARNING: THIS IS REALLY UNSAFE TO DECOMMENT THE "UnsafeImpure" module ! + + unsafe_coerce coerces an impure computation into a pure one ! + +*) + +(* START COMMENT *) + Module UnsafeImpure. + + Parameter unsafe_coerce: forall {A}, t A -> option A. + + Parameter unsafe_coerce_not_really_correct: forall A (k: t A) (x:A), (unsafe_coerce k)=Some x -> mayRet k x. + + Extraction Inline unsafe_coerce. + + End UnsafeImpure. +(* END COMMENT *) + + +End ImpureView. + + +Module Impure: ImpureView. + + Include IdentityMonad. + + Module UnsafeImpure. + + Definition unsafe_coerce {A} (x:t A) := Some x. + + Lemma unsafe_coerce_not_really_correct: forall A (k: t A) x, (unsafe_coerce k)=Some x -> mayRet k x. + Proof. + unfold unsafe_coerce, mayRet; congruence. + Qed. + + End UnsafeImpure. + +End Impure. + + +(** Comment the above code and decomment this to test that coq proofs still work with an impure monad ! + +- this should fail only on extraction or if unsafe_coerce is used ! + +*) +(* +Module Impure: MayReturnMonad := PowerSetMonad. +*) + +Export Impure. + +Extraction Inline ret mk_annot. + + +(* WARNING. The following directive is unsound. + + Extraction Inline bind + +For example, it may lead to extract the following code as "true" (instead of an error raising code) + failwith "foo";;true + +*) + +Extract Inlined Constant bind => "(|>)". + + +Extract Constant t "" => "". (* This weird directive extracts [t] as "'a" instead of "'a t" *) +Extraction Inline t. + +Global Opaque t. diff --git a/lib/Impure/ImpCore.v b/lib/Impure/ImpCore.v new file mode 100644 index 00000000..508b3f19 --- /dev/null +++ b/lib/Impure/ImpCore.v @@ -0,0 +1,196 @@ +(** Impure monad for interface with impure code + +*) + +Require Export Program. +Require Export ImpConfig. + +(* Theory: bind + embed => dbind + +Program Definition dbind {A B} (k1: t A) (k2: forall (a:A), (mayRet k1 a) -> t B) : t B + := bind (mk_annot k1) (fun a => k2 a _). + +Lemma mayRet_dbind: forall (A B:Type) k1 k2 (b:B), + mayRet (dbind k1 k2) b -> exists a:A, exists H: (mayRet k1 a), mayRet (k2 a H) b. +Proof. + intros A B k1 k2 b H; decompose [ex and] (mayRet_bind _ _ _ _ _ H). + eapply ex_intro. + eapply ex_intro. + eauto. +Qed. + +*) + +Definition wlp {A:Type} (k: t A) (P: A -> Prop): Prop + := forall a, mayRet k a -> P a. + +(* Notations *) + +(* Print Grammar constr. *) + +Module Notations. + + Bind Scope impure_scope with t. + Delimit Scope impure_scope with impure. + + Notation "?? A" := (t A) (at level 0, A at level 95): impure_scope. + + Notation "k '~~>' a" := (mayRet k a) (at level 75, no associativity): impure_scope. + + Notation "'RET' a" := (ret a) (at level 0): impure_scope. + + Notation "'DO' x '<~' k1 ';;' k2" := (bind k1 (fun x => k2)) + (at level 55, k1 at level 53, x at level 99, right associativity): impure_scope. + + Notation "k1 ';;' k2" := (bind k1 (fun _ => k2)) + (at level 55, right associativity): impure_scope. + + Notation "'WHEN' k '~>' a 'THEN' R" := (wlp k (fun a => R)) + (at level 73, R at level 100, right associativity): impure_scope. + + Notation "'ASSERT' P" := (ret (A:=P) _) (at level 0, only parsing): impure_scope. + +End Notations. + +Import Notations. +Local Open Scope impure. + +Goal ((?? list nat * ??nat -> nat) = ((?? ((list nat) * ?? nat) -> nat)))%type. +Proof. + apply refl_equal. +Qed. + + +(* wlp lemmas for tactics *) + +Lemma wlp_unfold A (k:??A)(P: A -> Prop): + (forall a, k ~~> a -> P a) + -> wlp k P. +Proof. + auto. +Qed. + +Lemma wlp_monotone A (k:?? A) (P1 P2: A -> Prop): + wlp k P1 + -> (forall a, k ~~> a -> P1 a -> P2 a) + -> wlp k P2. +Proof. + unfold wlp; eauto. +Qed. + +Lemma wlp_forall A B (k:?? A) (P: B -> A -> Prop): + (forall x, wlp k (P x)) + -> wlp k (fun a => forall x, P x a). +Proof. + unfold wlp; auto. +Qed. + +Lemma wlp_ret A (P: A -> Prop) a: + P a -> wlp (ret a) P. +Proof. + unfold wlp. + intros H b H0. + rewrite <- (mayRet_ret _ a b H0). + auto. +Qed. + +Lemma wlp_bind A B (k1:??A) (k2: A -> ??B) (P: B -> Prop): + wlp k1 (fun a => wlp (k2 a) P) -> wlp (bind k1 k2) P. +Proof. + unfold wlp. + intros H a H0. + case (mayRet_bind _ _ _ _ _ H0); clear H0. + intuition eauto. +Qed. + +Lemma wlp_ifbool A (cond: bool) (k1 k2: ?? A) (P: A -> Prop): + (cond=true -> wlp k1 P) -> (cond=false -> wlp k2 P) -> wlp (if cond then k1 else k2) P. +Proof. + destruct cond; auto. +Qed. + +Lemma wlp_letprod (A B C: Type) (p: A*B) (k: A -> B -> ??C) (P: C -> Prop): + (wlp (k (fst p) (snd p)) P) + -> (wlp (let (x,y):=p in (k x y)) P). +Proof. + destruct p; simpl; auto. +Qed. + +Lemma wlp_sum (A B C: Type) (x: A+B) (k1: A -> ??C) (k2: B -> ??C) (P: C -> Prop): + (forall a, x=inl a -> wlp (k1 a) P) -> + (forall b, x=inr b -> wlp (k2 b) P) -> + (wlp (match x with inl a => k1 a | inr b => k2 b end) P). +Proof. + destruct x; simpl; auto. +Qed. + +Lemma wlp_sumbool (A B:Prop) (C: Type) (x: {A}+{B}) (k1: A -> ??C) (k2: B -> ??C) (P: C -> Prop): + (forall a, x=left a -> wlp (k1 a) P) -> + (forall b, x=right b -> wlp (k2 b) P) -> + (wlp (match x with left a => k1 a | right b => k2 b end) P). +Proof. + destruct x; simpl; auto. +Qed. + +Lemma wlp_option (A B: Type) (x: option A) (k1: A -> ??B) (k2: ??B) (P: B -> Prop): + (forall a, x=Some a -> wlp (k1 a) P) -> + (x=None -> wlp k2 P) -> + (wlp (match x with Some a => k1 a | None => k2 end) P). +Proof. + destruct x; simpl; auto. +Qed. + +(* Tactics + +MAIN tactics: + - xtsimplify "base": simplification using from hints in "base" database (in particular "wlp" lemmas). + - xtstep "base": only one step of simplification. + +For good performance, it is recommanded to have several databases. + +*) + +Ltac introcomp := + let a:= fresh "exta" in + let H:= fresh "Hexta" in + intros a H. + +(* decompose the current wlp goal using "introduction" rules *) +Ltac wlp_decompose := + apply wlp_ret + || apply wlp_bind + || apply wlp_ifbool + || apply wlp_letprod + || apply wlp_sum + || apply wlp_sumbool + || apply wlp_option + . + +(* this tactic simplifies the current "wlp" goal using any hint found via tactic "hint". *) +Ltac apply_wlp_hint hint := + eapply wlp_monotone; + [ hint; fail | idtac ] ; + simpl; introcomp. + +(* one step of wlp_xsimplify +*) +Ltac wlp_step hint := + match goal with + | |- (wlp _ _) => + wlp_decompose + || apply_wlp_hint hint + || (apply wlp_unfold; introcomp) + end. + +(* main general tactic +WARNING: for the good behavior of "wlp_xsimplify", "hint" must at least perform a "eauto". + +Example of use: + wlp_xsimplify (intuition eauto with base). +*) +Ltac wlp_xsimplify hint := + repeat (intros; subst; wlp_step hint; simpl; (tauto || hint)). + +Create HintDb wlp discriminated. + +Ltac wlp_simplify := wlp_xsimplify ltac:(intuition eauto with wlp). diff --git a/lib/Impure/ImpExtern.v b/lib/Impure/ImpExtern.v new file mode 100644 index 00000000..8fb3cf3b --- /dev/null +++ b/lib/Impure/ImpExtern.v @@ -0,0 +1,7 @@ +(** Exporting Extern functions +*) + +Require Export ImpPrelude. +Require Export ImpIO. +Require Export ImpLoops. +Require Export ImpHCons. diff --git a/lib/Impure/ImpHCons.v b/lib/Impure/ImpHCons.v new file mode 100644 index 00000000..637116cc --- /dev/null +++ b/lib/Impure/ImpHCons.v @@ -0,0 +1,199 @@ +Require Export ImpIO. + +Import Notations. +Local Open Scope impure. + + +Axiom string_of_hashcode: hashcode -> ?? caml_string. +Extract Constant string_of_hashcode => "string_of_int". + +Axiom hash: forall {A}, A -> ?? hashcode. +Extract Constant hash => "Hashtbl.hash". + +(**************************) +(* (Weak) Sets *) + + +Import Dict. + +Axiom make_dict: forall {A B}, (hash_params A) -> ?? Dict.t A B. +Extract Constant make_dict => "ImpHConsOracles.make_dict". + + +Module Sets. + +Definition t {A} (mod: A -> Prop) := Dict.t A {x | mod x}. + +Definition empty {A} (hp: hash_params A) {mod:A -> Prop}: ?? t mod := + make_dict hp. + +Program Fixpoint add {A} (l: list A) {mod: A -> Prop} (d: t mod): forall {H:forall x, List.In x l -> mod x}, ?? unit := + match l with + | nil => fun H => RET () + | x::l' => fun H => + d.(set)(x,x);; + add l' d + end. + +Program Definition create {A} (hp: hash_params A) (l:list A): ?? t (fun x => List.In x l) := + DO d <~ empty hp (mod:=fun x => List.In x l);; + add l (mod:=fun x => List.In x l) d (H:=_);; + RET d. +Global Opaque create. + +Definition is_present {A} (hp: hash_params A) (x:A) {mod} (d:t mod): ?? bool := + DO oy <~ (d.(get)) x;; + match oy with + | Some y => hp.(test_eq) x (`y) + | None => RET false + end. + +Local Hint Resolve test_eq_correct: wlp. + +Lemma is_present_correct A (hp: hash_params A) x mod (d:t mod): + WHEN is_present hp x d ~> b THEN b=true -> mod x. +Proof. + wlp_simplify; subst; eauto. + - apply proj2_sig. + - discriminate. +Qed. +Hint Resolve is_present_correct: wlp. +Global Opaque is_present. + +Definition msg_assert_incl: pstring := "Sets.assert_incl". + +Fixpoint assert_incl {A} (hp: hash_params A) (l: list A) {mod} (d:t mod): ?? unit := + match l with + | nil => RET () + | x::l' => + DO b <~ is_present hp x d;; + if b then + assert_incl hp l' d + else ( + hp.(log) x;; + FAILWITH msg_assert_incl + ) + end. + +Lemma assert_incl_correct A (hp: hash_params A) l mod (d:t mod): + WHEN assert_incl hp l d ~> _ THEN forall x, List.In x l -> mod x. +Proof. + induction l; wlp_simplify; subst; eauto. +Qed. +Hint Resolve assert_incl_correct: wlp. +Global Opaque assert_incl. + +Definition assert_list_incl {A} (hp: hash_params A) (l1 l2: list A): ?? unit := + (* println "";;print("dict_create ");;*) + DO d <~ create hp l2;; + (*print("assert_incl ");;*) + assert_incl hp l1 d. + +Lemma assert_list_incl_correct A (hp: hash_params A) l1 l2: + WHEN assert_list_incl hp l1 l2 ~> _ THEN List.incl l1 l2. +Proof. + wlp_simplify. +Qed. +Global Opaque assert_list_incl. +Hint Resolve assert_list_incl_correct: wlp. + +End Sets. + + + + +(********************************) +(* (Weak) HConsing *) + +Module HConsing. + +Export HConsingDefs. + +(* NB: this axiom is NOT intended to be called directly, but only through [hCons...] functions below. *) +Axiom xhCons: forall {A}, (hashP A) -> ?? hashConsing A. +Extract Constant xhCons => "ImpHConsOracles.xhCons". + +Definition hCons_eq_msg: pstring := "xhCons: hash eq differs". + +Definition hCons {A} (hp: hashP A): ?? (hashConsing A) := + DO hco <~ xhCons hp ;; + RET {| + hC := (fun x => + DO x' <~ hC hco x ;; + DO b0 <~ hash_eq hp x.(hdata) x' ;; + assert_b b0 hCons_eq_msg;; + RET x'); + next_hid := hco.(next_hid); + next_log := hco.(next_log); + export := hco.(export); + remove := hco.(remove) + |}. + + +Lemma hCons_correct A (hp: hashP A): + WHEN hCons hp ~> hco THEN + (forall x y, WHEN hp.(hash_eq) x y ~> b THEN b=true -> (ignore_hid hp x)=(ignore_hid hp y)) -> + forall x, WHEN hco.(hC) x ~> x' THEN ignore_hid hp x.(hdata)=ignore_hid hp x'. +Proof. + wlp_simplify. +Qed. +Global Opaque hCons. +Hint Resolve hCons_correct: wlp. + + + +(* hashV: extending a given type with hash-consing *) +Record hashV {A:Type}:= { + data: A; + hid: hashcode +}. +Arguments hashV: clear implicits. + +Definition hashV_C {A} (test_eq: A -> A -> ?? bool) : hashP (hashV A) := {| + hash_eq := fun v1 v2 => test_eq v1.(data) v2.(data); + get_hid := hid; + set_hid := fun v id => {| data := v.(data); hid := id |} +|}. + +Definition liftHV (x:nat) := {| data := x; hid := unknown_hid |}. + +Definition hConsV {A} (hasheq: A -> A -> ?? bool): ?? (hashConsing (hashV A)) := + hCons (hashV_C hasheq). + +Lemma hConsV_correct A (hasheq: A -> A -> ?? bool): + WHEN hConsV hasheq ~> hco THEN + (forall x y, WHEN hasheq x y ~> b THEN b=true -> x=y) -> + forall x, WHEN hco.(hC) x ~> x' THEN x.(hdata).(data)=x'.(data). +Proof. + Local Hint Resolve f_equal2: core. + wlp_simplify. + exploit H; eauto. + + wlp_simplify. + + intros; congruence. +Qed. +Global Opaque hConsV. +Hint Resolve hConsV_correct: wlp. + +Definition hC_known {A} (hco:hashConsing (hashV A)) (unknownHash_msg: hashinfo (hashV A) -> ?? pstring) (x:hashinfo (hashV A)): ?? hashV A := + DO clock <~ hco.(next_hid)();; + DO x' <~ hco.(hC) x;; + DO ok <~ hash_older x'.(hid) clock;; + if ok + then RET x' + else + hco.(remove) x;; + DO msg <~ unknownHash_msg x;; + FAILWITH msg. + +Lemma hC_known_correct A (hco:hashConsing (hashV A)) msg x: + WHEN hC_known hco msg x ~> x' THEN + (forall x, WHEN hco.(hC) x ~> x' THEN x.(hdata).(data)=x'.(data)) -> + x.(hdata).(data)=x'.(data). +Proof. + wlp_simplify. + unfold wlp in * |- ; eauto. +Qed. +Global Opaque hC_known. +Hint Resolve hC_known_correct: wlp. + +End HConsing. diff --git a/lib/Impure/ImpIO.v b/lib/Impure/ImpIO.v new file mode 100644 index 00000000..6c02c395 --- /dev/null +++ b/lib/Impure/ImpIO.v @@ -0,0 +1,159 @@ +(** Extension of Coq language with some IO and exception-handling operators. + +TODO: integration with http://coq.io/ ? + +*) + +Require Export ImpPrelude. + +Import Notations. +Local Open Scope impure. + +(** Printing functions *) + +Axiom print: pstring -> ?? unit. +Extract Constant print => "ImpIOOracles.print". + +Axiom println: pstring -> ?? unit. +Extract Constant println => "ImpIOOracles.println". + +Axiom read_line: unit -> ?? pstring. +Extract Constant read_line => "ImpIOOracles.read_line". + +Require Import ZArith. +Axiom string_of_Z: Z -> ?? pstring. +Extract Constant string_of_Z => "ImpIOOracles.string_of_Z". + +(** timer *) + +Axiom timer: forall {A B}, (A -> ?? B)*A -> ?? B. +Extract Constant timer => "ImpIOOracles.timer". + +(** Exception Handling *) + +Axiom exit_observer: Type. +Extract Constant exit_observer => "((unit -> unit) ref)". + +Axiom new_exit_observer: (unit -> ??unit) -> ??exit_observer. +Extract Constant new_exit_observer => "ImpIOOracles.new_exit_observer". + +Axiom set_exit_observer: exit_observer * (unit -> ??unit) -> ??unit. +Extract Constant set_exit_observer => "ImpIOOracles.set_exit_observer". + +Axiom exn: Type. +Extract Inlined Constant exn => "exn". + +Axiom raise: forall {A}, exn -> ?? A. +Extract Constant raise => "raise". + +Axiom exn2string: exn -> ?? pstring. +Extract Constant exn2string => "ImpIOOracles.exn2string". + +Axiom fail: forall {A}, pstring -> ?? A. +Extract Constant fail => "ImpIOOracles.fail". + +Axiom try_with_fail: forall {A}, (unit -> ?? A) * (pstring -> exn -> ??A) -> ??A. +Extract Constant try_with_fail => "ImpIOOracles.try_with_fail". + +Axiom try_with_any: forall {A}, (unit -> ?? A) * (exn -> ??A) -> ??A. +Extract Constant try_with_any => "ImpIOOracles.try_with_any". + +Notation "'RAISE' e" := (DO r <~ raise (A:=False) e ;; RET (match r with end)) (at level 0): impure_scope. +Notation "'FAILWITH' msg" := (DO r <~ fail (A:=False) msg ;; RET (match r with end)) (at level 0): impure_scope. + +Definition _FAILWITH {A:Type} msg: ?? A := FAILWITH msg. + +Example _FAILWITH_correct A msg (P: A -> Prop): + WHEN _FAILWITH msg ~> r THEN P r. +Proof. + wlp_simplify. +Qed. + +Notation "'TRY' k1 'WITH_FAIL' s ',' e '=>' k2" := (try_with_fail (fun _ => k1, fun s e => k2)) + (at level 55, k1 at level 53, right associativity): impure_scope. + +Notation "'TRY' k1 'WITH_ANY' e '=>' k2" := (try_with_any (fun _ => k1, fun e => k2)) + (at level 55, k1 at level 53, right associativity): impure_scope. + + +Program Definition assert_b (b: bool) (msg: pstring): ?? b=true := + match b with + | true => RET _ + | false => FAILWITH msg + end. + +Lemma assert_wlp_true msg b: WHEN assert_b b msg ~> _ THEN b=true. +Proof. + wlp_simplify. +Qed. + +Lemma assert_false_wlp msg (P: Prop): WHEN assert_b false msg ~> _ THEN P. +Proof. + simpl; wlp_simplify. +Qed. + +Program Definition try_catch_fail_ensure {A} (k1: unit -> ?? A) (k2: pstring -> exn -> ??A) (P: A -> Prop | wlp (k1 tt) P /\ (forall s e, wlp (k2 s e) P)): ?? { r | P r } + := TRY + DO r <~ mk_annot (k1 tt);; + RET (exist P r _) + WITH_FAIL s, e => + DO r <~ mk_annot (k2 s e);; + RET (exist P r _). +Obligation 2. + unfold wlp in * |- *; eauto. +Qed. + +Notation "'TRY' k1 'CATCH_FAIL' s ',' e '=>' k2 'ENSURE' P" := (try_catch_fail_ensure (fun _ => k1) (fun s e => k2) (exist _ P _)) + (at level 55, k1 at level 53, right associativity): impure_scope. + +Definition is_try_post {A} (P: A -> Prop) k1 k2 : Prop := + wlp (k1 ()) P /\ forall (e:exn), wlp (k2 e) P. + +Program Definition try_catch_ensure {A} k1 k2 (P:A->Prop|is_try_post P k1 k2): ?? { r | P r } + := TRY + DO r <~ mk_annot (k1 ());; + RET (exist P r _) + WITH_ANY e => + DO r <~ mk_annot (k2 e);; + RET (exist P r _). +Obligation 1. + unfold is_try_post, wlp in * |- *; intuition eauto. +Qed. +Obligation 2. + unfold is_try_post, wlp in * |- *; intuition eauto. +Qed. + +Notation "'TRY' k1 'CATCH' e '=>' k2 'ENSURE' P" := (try_catch_ensure (fun _ => k1) (fun e => k2) (exist _ P _)) + (at level 55, k1 at level 53, right associativity): impure_scope. + + +Program Example tryex {A} (x y:A) := + TRY (RET x) + CATCH _ => (RET y) + ENSURE (fun r => r = x \/ r = y). +Obligation 1. + split; wlp_simplify. +Qed. + +Program Example tryex_test {A} (x y:A): + WHEN tryex x y ~> r THEN `r <> x -> `r = y. +Proof. + wlp_simplify. destruct exta as [r [X|X]]; intuition. +Qed. + + +Program Example try_branch1 {A} (x:A): ?? { r | r = x} := + TRY (RET x) + CATCH e => (FAILWITH "!") + ENSURE _. +Obligation 1. + split; wlp_simplify. +Qed. + +Program Example try_branch2 {A} (x:A): ?? { r | r = x} := + TRY (FAILWITH "!") + CATCH e => (RET x) + ENSURE _. +Obligation 1. + split; wlp_simplify. +Qed. diff --git a/lib/Impure/ImpLoops.v b/lib/Impure/ImpLoops.v new file mode 100644 index 00000000..33376c19 --- /dev/null +++ b/lib/Impure/ImpLoops.v @@ -0,0 +1,123 @@ +(** Extension of Coq language with generic loops. *) + +Require Export ImpIO. + +Import Notations. +Local Open Scope impure. + + +(** While-loop iterations *) + +Axiom loop: forall {A B}, A * (A -> ?? (A+B)) -> ?? B. +Extract Constant loop => "ImpLoopOracles.loop". + + +Section While_Loop. + +(** Local Definition of "while-loop-invariant" *) +Let wli {S} cond body (I: S -> Prop) := forall s, I s -> cond s = true -> WHEN (body s) ~> s' THEN I s'. + +Program Definition while {S} cond body (I: S -> Prop | wli cond body I) s0: ?? {s | (I s0 -> I s) /\ cond s = false} + := loop (A:={s | I s0 -> I s}) + (s0, + fun s => + match (cond s) with + | true => + DO s' <~ mk_annot (body s) ;; + RET (inl (A:={s | I s0 -> I s }) s') + | false => + RET (inr (B:={s | (I s0 -> I s) /\ cond s = false}) s) + end). +Obligation 2. + unfold wli, wlp in * |-; eauto. +Qed. +Extraction Inline while. + +End While_Loop. + + +Section Loop_Until_None. +(** useful to demonstrate a UNSAT property *) + +(** Local Definition of "loop-until-None-invariant" *) +Let luni {S} (body: S -> ?? (option S)) (I: S -> Prop) := forall s, I s -> WHEN (body s) ~> s' THEN match s' with Some s1 => I s1 | None => False end. + +Program Definition loop_until_None {S} body (I: S -> Prop | luni body I) s0: ?? ~(I s0) + := loop (A:={s | I s0 -> I s}) + (s0, + fun s => + DO s' <~ mk_annot (body s) ;; + match s' with + | Some s1 => RET (inl (A:={s | I s0 -> I s }) s1) + | None => RET (inr (B:=~(I s0)) _) + end). +Obligation 2. + refine (H2 s _ _ H0). auto. +Qed. +Obligation 3. + intros X; refine (H1 s _ _ H). auto. +Qed. +Extraction Inline loop_until_None. + +End Loop_Until_None. + + +(*********************************************) +(* A generic fixpoint from an equality test *) + +Record answ {A B: Type} {R: A -> B -> Prop} := { + input: A ; + output: B ; + correct: R input output +}. +Arguments answ {A B}. + +Definition msg: pstring := "wapply fails". + +Definition beq_correct {A} (beq: A -> A -> ?? bool) := + forall x y, WHEN beq x y ~> b THEN b=true -> x=y. + +Definition wapply {A B} {R: A -> B -> Prop} (beq: A -> A -> ?? bool) (k: A -> ?? answ R) (x:A): ?? B := + DO a <~ k x;; + DO b <~ beq x (input a) ;; + assert_b b msg;; + RET (output a). + +Lemma wapply_correct A B (R: A -> B -> Prop) (beq: A -> A -> ?? bool) (k: A -> ?? answ R) x: + beq_correct beq + -> WHEN wapply beq k x ~> y THEN R x y. +Proof. + unfold beq_correct; wlp_simplify. + destruct exta; simpl; auto. +Qed. +Local Hint Resolve wapply_correct: wlp. +Global Opaque wapply. + +Axiom xrec_set_option: recMode -> ?? unit. +Extract Constant xrec_set_option => "ImpLoopOracles.xrec_set_option". + +(* TODO: generalizaton to get beq (and a Hash function ?) in parameters ? *) +Axiom xrec: forall {A B}, ((A -> ?? B) -> A -> ?? B) -> ?? (A -> ?? B). +Extract Constant xrec => "ImpLoopOracles.xrec". + +Definition rec_preserv {A B} (recF: (A -> ?? B) -> A -> ?? B) (R: A -> B -> Prop) := + forall f x, WHEN recF f x ~> z THEN (forall x', WHEN f x' ~> y THEN R x' y) -> R x z. + + +Program Definition rec {A B} beq recF (R: A -> B -> Prop) (H1: rec_preserv recF R) (H2: beq_correct beq): ?? (A -> ?? B) := + DO f <~ xrec (B:=answ R) (fun f x => + DO y <~ mk_annot (recF (wapply beq f) x) ;; + RET {| input := x; output := `y |});; + RET (wapply beq f). +Obligation 1. + eapply H1; eauto. clear H H1. + wlp_simplify. +Qed. + +Lemma rec_correct A B beq recF (R: A -> B -> Prop) (H1: rec_preserv recF R) (H2: beq_correct beq): + WHEN rec beq recF R H1 H2 ~> f THEN forall x, WHEN f x ~> y THEN R x y. +Proof. + wlp_simplify. +Qed. +Hint Resolve rec_correct: wlp. +Global Opaque rec. diff --git a/lib/Impure/ImpMonads.v b/lib/Impure/ImpMonads.v new file mode 100644 index 00000000..f01a2755 --- /dev/null +++ b/lib/Impure/ImpMonads.v @@ -0,0 +1,148 @@ +(** Impure monad for interface with impure code +*) + + +Require Import Program. + + +Module Type MayReturnMonad. + + Axiom t: Type -> Type. + + Axiom mayRet: forall {A:Type}, t A -> A -> Prop. + + Axiom ret: forall {A}, A -> t A. + + Axiom bind: forall {A B}, (t A) -> (A -> t B) -> t B. + + Axiom mk_annot: forall {A} (k: t A), t { a: A | mayRet k a }. + + Axiom mayRet_ret: forall A (a b:A), + mayRet (ret a) b -> a=b. + + Axiom mayRet_bind: forall A B k1 k2 (b:B), + mayRet (bind k1 k2) b -> exists a:A, mayRet k1 a /\ mayRet (k2 a) b. + +End MayReturnMonad. + + + +(** Model of impure computation as predicate *) +Module PowerSetMonad<: MayReturnMonad. + + Definition t (A:Type) := A -> Prop. + + Definition mayRet {A:Type} (k: t A) a: Prop := k a. + + Definition ret {A:Type} (a:A) := eq a. + + Definition bind {A B:Type} (k1: t A) (k2: A -> t B) := + fun b => exists a, k1 a /\ k2 a b. + + Definition mk_annot {A} (k: t A) : t { a | mayRet k a } := fun _ => True. + + Lemma mayRet_ret A (a b:A): mayRet (ret a) b -> a=b. + Proof. + unfold mayRet, ret. firstorder. + Qed. + + Lemma mayRet_bind A B k1 k2 (b:B): + mayRet (bind k1 k2) b -> exists (a:A), mayRet k1 a /\ mayRet (k2 a) b. + Proof. + unfold mayRet, bind. + firstorder. + Qed. + +End PowerSetMonad. + + +(** The identity interpretation *) +Module IdentityMonad<: MayReturnMonad. + + Definition t (A:Type) := A. + + (* may-return semantics of computations *) + Definition mayRet {A:Type} (a b:A): Prop := a=b. + + Definition ret {A:Type} (a:A) := a. + + Definition bind {A B:Type} (k1: A) (k2: A -> B) := k2 k1. + + Definition mk_annot {A} (k: t A) : t { a: A | mayRet k a } + := exist _ k (eq_refl k) . + + Lemma mayRet_ret (A:Type) (a b:A): mayRet (ret a) b -> a=b. + Proof. + intuition. + Qed. + + Lemma mayRet_bind (A B:Type) (k1:t A) k2 (b:B): + mayRet (bind k1 k2) b -> exists (a:A), mayRet k1 a /\ mayRet (k2 a) b. + Proof. + firstorder. + Qed. + +End IdentityMonad. + + +(** Model of impure computation as state-transformers *) +Module StateMonad<: MayReturnMonad. + + Parameter St: Type. (* A global state *) + + Definition t (A:Type) := St -> A * St. + + Definition mayRet {A:Type} (k: t A) a: Prop := + exists s, fst (k s)=a. + + Definition ret {A:Type} (a:A) := fun (s:St) => (a,s). + + Definition bind {A B:Type} (k1: t A) (k2: A -> t B) := + fun s0 => let r := k1 s0 in k2 (fst r) (snd r). + + Program Definition mk_annot {A} (k: t A) : t { a | mayRet k a } := + fun s0 => let r := k s0 in (exist _ (fst r) _, snd r). + Obligation 1. + unfold mayRet; eauto. + Qed. + + Lemma mayRet_ret {A:Type} (a b:A): mayRet (ret a) b -> a=b. + Proof. + unfold mayRet, ret. firstorder. + Qed. + + Lemma mayRet_bind {A B:Type} k1 k2 (b:B): + mayRet (bind k1 k2) b -> exists (a:A), mayRet k1 a /\ mayRet (k2 a) b. + Proof. + unfold mayRet, bind. firstorder eauto. + Qed. + +End StateMonad. + +(** The deferred interpretation *) +Module DeferredMonad<: MayReturnMonad. + + Definition t (A:Type) := unit -> A. + + (* may-return semantics of computations *) + Definition mayRet {A:Type} (a: t A) (b:A): Prop := a tt=b. + + Definition ret {A:Type} (a:A) : t A := fun _ => a. + + Definition bind {A B:Type} (k1: t A) (k2: A -> t B) : t B := fun _ => k2 (k1 tt) tt. + + Definition mk_annot {A} (k: t A) : t { a: A | mayRet k a } + := fun _ => exist _ (k tt) (eq_refl (k tt)). + + Lemma mayRet_ret (A:Type) (a b: A): mayRet (ret a) b -> a=b. + Proof. + intuition. + Qed. + + Lemma mayRet_bind (A B:Type) (k1:t A) k2 (b:B): + mayRet (bind k1 k2) b -> exists (a:A), mayRet k1 a /\ mayRet (k2 a) b. + Proof. + firstorder. + Qed. + +End DeferredMonad. diff --git a/lib/Impure/ImpPrelude.v b/lib/Impure/ImpPrelude.v new file mode 100644 index 00000000..de4c7973 --- /dev/null +++ b/lib/Impure/ImpPrelude.v @@ -0,0 +1,206 @@ +Require Export String. +Require Export List. +Require Extraction. +Require Import Ascii. +Require Import BinNums. +Require Export ImpCore. +Require Export PArith. + + +Import Notations. +Local Open Scope impure. + +(** Impure lazy andb of booleans *) +Definition iandb (k1 k2: ??bool): ?? bool := + DO r1 <~ k1 ;; + if r1 then k2 else RET false. + +Extraction Inline iandb. (* Juste pour l'efficacité à l'extraction ! *) + +(** Strings for pretty-printing *) + +Axiom caml_string: Type. +Extract Constant caml_string => "string". + +(* New line *) +Definition nl: string := String (ascii_of_pos 10%positive) EmptyString. + +Inductive pstring: Type := + | Str: string -> pstring + | CamlStr: caml_string -> pstring + | Concat: pstring -> pstring -> pstring. + +Coercion Str: string >-> pstring. +Bind Scope string_scope with pstring. + +Notation "x +; y" := (Concat x y) + (at level 65, left associativity): string_scope. + +(** Coq references *) + +Record cref {A} := { + set: A -> ?? unit; + get: unit -> ?? A +}. +Arguments cref: clear implicits. + +Axiom make_cref: forall {A}, A -> ?? cref A. +Extract Constant make_cref => "(fun x -> let r = ref x in { set = (fun y -> r:=y); get = (fun () -> !r) })". + + +(** Data-structure for a logger *) + +Record logger {A:Type} := { + log_insert: A -> ?? unit; + log_info: unit -> ?? pstring; +}. +Arguments logger: clear implicits. + +Axiom count_logger: unit -> ?? logger unit. +Extract Constant count_logger => "(fun () -> let count = ref 0 in { log_insert = (fun () -> count := !count + 1); log_info = (fun () -> (CamlStr (string_of_int !count))) })". + + +(** Axioms of Physical equality *) + +Axiom phys_eq: forall {A}, A -> A -> ?? bool. + +Axiom phys_eq_correct: forall A (x y:A), WHEN phys_eq x y ~> b THEN b=true -> x=y. + + +(* We only check here that above axioms are not trivially inconsistent... + (but this does not prove the correctness of the extraction directive below). + *) +Module PhysEqModel. + +Definition phys_eq {A} (x y: A) := ret false. + +Lemma phys_eq_correct: forall A (x y:A), WHEN phys_eq x y ~> b THEN b=true -> x=y. +Proof. + wlp_simplify. discriminate. +Qed. + +End PhysEqModel. + +Extract Inlined Constant phys_eq => "(==)". +Hint Resolve phys_eq_correct: wlp. + + +Axiom struct_eq: forall {A}, A -> A -> ?? bool. +Axiom struct_eq_correct: forall A (x y:A), WHEN struct_eq x y ~> b THEN if b then x=y else x<>y. +Extract Inlined Constant struct_eq => "(=)". +Hint Resolve struct_eq_correct: wlp. + + +(** Data-structure for generic hash-consing *) + +Axiom hashcode: Type. +Extract Constant hashcode => "int". + +(* NB: hashConsing is assumed to generate hash-code in ascending order. + This gives a way to check that a hash-consed value is older than an other one. +*) +Axiom hash_older: hashcode -> hashcode -> ?? bool. +Extract Inlined Constant hash_older => "(<)". + +Module Dict. + +Record hash_params {A:Type} := { + test_eq: A -> A -> ??bool; + test_eq_correct: forall x y, WHEN test_eq x y ~> r THEN r=true -> x=y; + hashing: A -> ??hashcode; + log: A -> ??unit (* for debugging only *) +}. +Arguments hash_params: clear implicits. + + +Record t {A B:Type} := { + set: A * B -> ?? unit; + get: A -> ?? option B +}. +Arguments t: clear implicits. + +End Dict. + +Module HConsingDefs. + +Record hashinfo {A: Type} := { + hdata: A; + hcodes: list hashcode; +}. +Arguments hashinfo: clear implicits. + +(* for inductive types with intrinsic hash-consing *) +Record hashP {A:Type}:= { + hash_eq: A -> A -> ?? bool; + get_hid: A -> hashcode; + set_hid: A -> hashcode -> A; (* WARNING: should only be used by hash-consing machinery *) +}. +Arguments hashP: clear implicits. + +Axiom unknown_hid: hashcode. +Extract Constant unknown_hid => "-1". + +Definition ignore_hid {A} (hp: hashP A) (hv:A) := set_hid hp hv unknown_hid. + +Record hashExport {A:Type}:= { + get_info: hashcode -> ?? hashinfo A; + iterall: ((list pstring) -> hashcode -> hashinfo A -> ?? unit) -> ?? unit; (* iter on all elements in the hashtbl, by order of creation *) +}. +Arguments hashExport: clear implicits. + +Record hashConsing {A:Type}:= { + hC: hashinfo A -> ?? A; + (**** below: debugging or internal functions ****) + next_hid: unit -> ?? hashcode; (* should be strictly less old than ignore_hid *) + remove: hashinfo A -> ??unit; (* SHOULD NOT BE USED ! *) + next_log: pstring -> ?? unit; (* insert a log info (for the next introduced element) -- regiven by [iterall export] below *) + export: unit -> ?? hashExport A ; +}. +Arguments hashConsing: clear implicits. + +End HConsingDefs. + +(** recMode: this is mainly for Tests ! *) +Inductive recMode:= StdRec | MemoRec | BareRec | BuggyRec. + + +(* This a copy-paste from definitions in CompCert/Lib/CoqLib.v *) +Lemma modusponens: forall (P Q: Prop), P -> (P -> Q) -> Q. +Proof. auto. Qed. + +Ltac exploit x := + refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) + || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) + || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) + || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) + || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) + || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) + || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) + || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) + || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) + || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) + || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) + || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) + || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) + || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) + || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) + || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) + || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) + || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) + || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) + || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) + || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) + || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _ _) _) + || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _ _) _) + || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _ _) _) + || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _ _) _) + || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _ _) _) + || refine (modusponens _ _ (x _ _ _ _ _ _ _ _ _) _) + || refine (modusponens _ _ (x _ _ _ _ _ _ _ _) _) + || refine (modusponens _ _ (x _ _ _ _ _ _ _) _) + || refine (modusponens _ _ (x _ _ _ _ _ _) _) + || refine (modusponens _ _ (x _ _ _ _ _) _) + || refine (modusponens _ _ (x _ _ _ _) _) + || refine (modusponens _ _ (x _ _ _) _) + || refine (modusponens _ _ (x _ _) _) + || refine (modusponens _ _ (x _) _). diff --git a/lib/Impure/LICENSE b/lib/Impure/LICENSE new file mode 100644 index 00000000..65c5ca88 --- /dev/null +++ b/lib/Impure/LICENSE @@ -0,0 +1,165 @@ + GNU LESSER GENERAL PUBLIC LICENSE + Version 3, 29 June 2007 + + Copyright (C) 2007 Free Software Foundation, Inc. <http://fsf.org/> + Everyone is permitted to copy and distribute verbatim copies + of this license document, but changing it is not allowed. + + + This version of the GNU Lesser General Public License incorporates +the terms and conditions of version 3 of the GNU General Public +License, supplemented by the additional permissions listed below. + + 0. Additional Definitions. + + As used herein, "this License" refers to version 3 of the GNU Lesser +General Public License, and the "GNU GPL" refers to version 3 of the GNU +General Public License. + + "The Library" refers to a covered work governed by this License, +other than an Application or a Combined Work as defined below. + + An "Application" is any work that makes use of an interface provided +by the Library, but which is not otherwise based on the Library. +Defining a subclass of a class defined by the Library is deemed a mode +of using an interface provided by the Library. + + A "Combined Work" is a work produced by combining or linking an +Application with the Library. The particular version of the Library +with which the Combined Work was made is also called the "Linked +Version". + + The "Minimal Corresponding Source" for a Combined Work means the +Corresponding Source for the Combined Work, excluding any source code +for portions of the Combined Work that, considered in isolation, are +based on the Application, and not on the Linked Version. + + The "Corresponding Application Code" for a Combined Work means the +object code and/or source code for the Application, including any data +and utility programs needed for reproducing the Combined Work from the +Application, but excluding the System Libraries of the Combined Work. + + 1. Exception to Section 3 of the GNU GPL. + + You may convey a covered work under sections 3 and 4 of this License +without being bound by section 3 of the GNU GPL. + + 2. Conveying Modified Versions. + + If you modify a copy of the Library, and, in your modifications, a +facility refers to a function or data to be supplied by an Application +that uses the facility (other than as an argument passed when the +facility is invoked), then you may convey a copy of the modified +version: + + a) under this License, provided that you make a good faith effort to + ensure that, in the event an Application does not supply the + function or data, the facility still operates, and performs + whatever part of its purpose remains meaningful, or + + b) under the GNU GPL, with none of the additional permissions of + this License applicable to that copy. + + 3. Object Code Incorporating Material from Library Header Files. + + The object code form of an Application may incorporate material from +a header file that is part of the Library. You may convey such object +code under terms of your choice, provided that, if the incorporated +material is not limited to numerical parameters, data structure +layouts and accessors, or small macros, inline functions and templates +(ten or fewer lines in length), you do both of the following: + + a) Give prominent notice with each copy of the object code that the + Library is used in it and that the Library and its use are + covered by this License. + + b) Accompany the object code with a copy of the GNU GPL and this license + document. + + 4. Combined Works. + + You may convey a Combined Work under terms of your choice that, +taken together, effectively do not restrict modification of the +portions of the Library contained in the Combined Work and reverse +engineering for debugging such modifications, if you also do each of +the following: + + a) Give prominent notice with each copy of the Combined Work that + the Library is used in it and that the Library and its use are + covered by this License. + + b) Accompany the Combined Work with a copy of the GNU GPL and this license + document. + + c) For a Combined Work that displays copyright notices during + execution, include the copyright notice for the Library among + these notices, as well as a reference directing the user to the + copies of the GNU GPL and this license document. + + d) Do one of the following: + + 0) Convey the Minimal Corresponding Source under the terms of this + License, and the Corresponding Application Code in a form + suitable for, and under terms that permit, the user to + recombine or relink the Application with a modified version of + the Linked Version to produce a modified Combined Work, in the + manner specified by section 6 of the GNU GPL for conveying + Corresponding Source. + + 1) Use a suitable shared library mechanism for linking with the + Library. A suitable mechanism is one that (a) uses at run time + a copy of the Library already present on the user's computer + system, and (b) will operate properly with a modified version + of the Library that is interface-compatible with the Linked + Version. + + e) Provide Installation Information, but only if you would otherwise + be required to provide such information under section 6 of the + GNU GPL, and only to the extent that such information is + necessary to install and execute a modified version of the + Combined Work produced by recombining or relinking the + Application with a modified version of the Linked Version. (If + you use option 4d0, the Installation Information must accompany + the Minimal Corresponding Source and Corresponding Application + Code. If you use option 4d1, you must provide the Installation + Information in the manner specified by section 6 of the GNU GPL + for conveying Corresponding Source.) + + 5. Combined Libraries. + + You may place library facilities that are a work based on the +Library side by side in a single library together with other library +facilities that are not Applications and are not covered by this +License, and convey such a combined library under terms of your +choice, if you do both of the following: + + a) Accompany the combined library with a copy of the same work based + on the Library, uncombined with any other library facilities, + conveyed under the terms of this License. + + b) Give prominent notice with the combined library that part of it + is a work based on the Library, and explaining where to find the + accompanying uncombined form of the same work. + + 6. Revised Versions of the GNU Lesser General Public License. + + The Free Software Foundation may publish revised and/or new versions +of the GNU Lesser General Public License from time to time. Such new +versions will be similar in spirit to the present version, but may +differ in detail to address new problems or concerns. + + Each version is given a distinguishing version number. If the +Library as you received it specifies that a certain numbered version +of the GNU Lesser General Public License "or any later version" +applies to it, you have the option of following the terms and +conditions either of that published version or of any later version +published by the Free Software Foundation. If the Library as you +received it does not specify a version number of the GNU Lesser +General Public License, you may choose any version of the GNU Lesser +General Public License ever published by the Free Software Foundation. + + If the Library as you received it specifies that a proxy can decide +whether future versions of the GNU Lesser General Public License shall +apply, that proxy's public statement of acceptance of any version is +permanent authorization for you to choose that version for the +Library. diff --git a/lib/Impure/README.md b/lib/Impure/README.md new file mode 100644 index 00000000..2b19d14a --- /dev/null +++ b/lib/Impure/README.md @@ -0,0 +1,31 @@ +# `Impure`: importing OCaml functions as non-deterministic ones. + +The principle of this library is to encode the type `A -> B` of an +OCaml function as a type `A -> ?? B` in Coq, where `?? B` is the type +of an axiomatized monad that can be interpreted as `B -> Prop`. In +other word, this encoding abstracts an OCaml function as a function +returning a postcondition on its possible results (ie a relation between its +parameter and its result). Side-effects are simply ignored. And +reasoning on such a function is only possible in partial correctness. + +See further explanations and examples on [ImpureDemo](https://github.com/boulme/ImpureDemo). + +## Credits + +[Sylvain Boulmé](mailto:Sylvain.Boulme@univ-grenoble-alpes.fr). + +## Code Overview + +- [ImpMonads](ImpMonads.v) axioms of "impure computations" and some Coq models of these axioms. + +- [ImpConfig](ImpConfig.v) declares the `Impure` monad and defines its extraction. + +- [ImpCore](ImpCore.v) defines notations for the `Impure` monad and a `wlp_simplify` tactic (to reason about `Impure` functions in a Hoare-logic style). + +- [ImpPrelude](ImpPrelude.v) declares the data types exchanged with `Impure` oracles. + +- [ImpIO](ImpIO.v), [ImpLoops](ImpLoops.v), [ImpHCons](ImpHCons.v) declare `Impure` oracles and define operators from these oracles. + [ImpExtern](ImpExtern.v) exports all these impure operators. + +- [ocaml/](ocaml/) subdirectory containing the OCaml implementations of `Impure` oracles. + diff --git a/lib/Impure/ocaml/ImpHConsOracles.ml b/lib/Impure/ocaml/ImpHConsOracles.ml new file mode 100644 index 00000000..68a33a91 --- /dev/null +++ b/lib/Impure/ocaml/ImpHConsOracles.ml @@ -0,0 +1,72 @@ +open ImpPrelude +open HConsingDefs + +let make_dict (type key) (p: key Dict.hash_params) = + let module MyHashedType = struct + type t = key + let equal = p.Dict.test_eq + let hash = p.Dict.hashing + end in + let module MyHashtbl = Hashtbl.Make(MyHashedType) in + let dict = MyHashtbl.create 1000 in + { + Dict.set = (fun (k,d) -> MyHashtbl.replace dict k d); + Dict.get = (fun k -> MyHashtbl.find_opt dict k) + } + + +exception Stop;; + +let xhCons (type a) (hp:a hashP) = + (* We use a hash-table, but a hash-set would be sufficient ! *) + (* Thus, we could use a weak hash-set, but prefer avoid it for easier debugging *) + (* Ideally, a parameter would allow to select between the weak or full version *) + let module MyHashedType = struct + type t = a hashinfo + let equal x y = hp.hash_eq x.hdata y.hdata + let hash x = Hashtbl.hash x.hcodes + end in + let module MyHashtbl = Hashtbl.Make(MyHashedType) in + let pick t = + let res = ref None in + try + MyHashtbl.iter (fun k d -> res:=Some (k,d); raise Stop) t; + None + with + | Stop -> !res + in + let t = MyHashtbl.create 1000 in + let logs = ref [] in + { + hC = (fun (k:a hashinfo) -> + (* DEBUG: + Printf.printf "*in %d -- look for hcodes= " (Obj.magic t); + List.iter (fun i -> Printf.printf "%d " i) k.hcodes; + print_newline(); + *) + match MyHashtbl.find_opt t k with + | Some d -> d + | None -> + (* DEBUG: Printf.printf "*in %d -- new hid:%d" (Obj.magic t) (MyHashtbl.length t); print_newline(); *) + let d = hp.set_hid k.hdata (MyHashtbl.length t) in + MyHashtbl.add t {k with hdata = d } d; d); + next_log = (fun info -> logs := (MyHashtbl.length t, info)::(!logs)); + next_hid = (fun () -> MyHashtbl.length t); + remove = (fun (x:a hashinfo) -> MyHashtbl.remove t x); + export = fun () -> + match pick t with + | None -> { get_info = (fun _ -> raise Not_found); iterall = (fun _ -> ()) } + | Some (k,_) -> + (* the state is fully copied at export ! *) + let logs = ref (List.rev_append (!logs) []) in + let rec step_log i = + match !logs with + | (j, info)::l' when i>=j -> logs:=l'; info::(step_log i) + | _ -> [] + in let a = Array.make (MyHashtbl.length t) k in + MyHashtbl.iter (fun k d -> a.(hp.get_hid d) <- k) t; + { + get_info = (fun i -> a.(i)); + iterall = (fun iter_node -> Array.iteri (fun i k -> iter_node (step_log i) i k) a) + } + } diff --git a/lib/Impure/ocaml/ImpHConsOracles.mli b/lib/Impure/ocaml/ImpHConsOracles.mli new file mode 100644 index 00000000..5075d176 --- /dev/null +++ b/lib/Impure/ocaml/ImpHConsOracles.mli @@ -0,0 +1,5 @@ +open ImpPrelude +open HConsingDefs + +val make_dict : 'a Dict.hash_params -> ('a, 'b) Dict.t +val xhCons: 'a hashP -> 'a hashConsing diff --git a/lib/Impure/ocaml/ImpIOOracles.ml b/lib/Impure/ocaml/ImpIOOracles.ml new file mode 100644 index 00000000..9e63c12d --- /dev/null +++ b/lib/Impure/ocaml/ImpIOOracles.ml @@ -0,0 +1,142 @@ +(* Warning + +These oracles assumes the following extraction directives: + "Require Import ExtrOcamlString." + +*) + +open ImpPrelude +(* +open BinNums +open Datatypes +*) + +(* two auxiliary functions, for efficient mapping of "int" to "BinNums.positive" *) +exception Overflow + +let aux_add: ('a, 'b) Hashtbl.t -> 'b Queue.t -> 'a -> 'b -> unit + = fun t q i p -> + if i < 1 then (* protection against wrap around *) + raise Overflow; + Queue.add p q; + Hashtbl.add t i p + +let memo_int2pos: int -> int -> BinNums.positive + = fun n -> + (* init of the Hashtbl *) + let n = max n 1 in + let t = Hashtbl.create n in + let q = Queue.create () in + aux_add t q 1 BinNums.Coq_xH ; + for i = 1 to (n-1)/2 do + let last = Queue.take q in + let ni = 2*i in + aux_add t q ni (BinNums.Coq_xO last); + aux_add t q (ni+1) (BinNums.Coq_xI last) + done; + if n mod 2 = 0 then ( + let last = Queue.take q in + Hashtbl.add t n (BinNums.Coq_xO last) + ); + (* memoized translation of i *) + let rec find i = + try + (* Printf.printf "-> %d\n" i; *) + Hashtbl.find t i + with Not_found -> + (* Printf.printf "<- %d\n" i; *) + if i <= 0 then + invalid_arg "non-positive integer" + else + let p = find (i/2) in + let pi = if i mod 2 = 0 then BinNums.Coq_xO p else BinNums.Coq_xI p in + Hashtbl.add t i pi; + pi + in find;; + +let new_exit_observer: (unit -> unit) -> (unit -> unit) ref + = fun f -> + let o = ref f in + at_exit (fun () -> !o()); + o;; + +let set_exit_observer: (unit -> unit) ref * (unit -> unit) -> unit + = fun (r, f) -> r := f + +let rec print: pstring -> unit + = fun ps -> + match ps with + | Str l -> List.iter print_char l + | CamlStr s -> print_string s + | Concat(ps1,ps2) -> (print ps1; print ps2);; + +let println: pstring -> unit + = fun l -> print l; print_newline() + +let read_line () = + CamlStr (Stdlib.read_line());; + +exception ImpureFail of pstring;; + +let exn2string: exn -> pstring + = fun e -> CamlStr (Printexc.to_string e) + +let fail: pstring -> 'a + = fun s -> raise (ImpureFail s);; + +let try_with_fail: (unit -> 'a) * (pstring -> exn -> 'a) -> 'a + = fun (k1, k2) -> + try + k1() + with + | (ImpureFail s) as e -> k2 s e + +let try_with_any: (unit -> 'a) * (exn -> 'a) -> 'a + = fun (k1, k2) -> + try + k1() + with + | e -> k2 e + +(** MISC **) + +let rec posTr: BinNums.positive -> int += function + | BinNums.Coq_xH -> 1 + | BinNums.Coq_xO p -> (posTr p)*2 + | BinNums.Coq_xI p -> (posTr p)*2+1;; + +let zTr: BinNums.coq_Z -> int += function + | BinNums.Z0 -> 0 + | BinNums.Zpos p -> posTr p + | BinNums.Zneg p -> - (posTr p) + +let ten = BinNums.Zpos (BinNums.Coq_xO (BinNums.Coq_xI (BinNums.Coq_xO BinNums.Coq_xH))) + +let rec string_of_pos (p:BinNums.positive) (acc: pstring): pstring += let (q,r) = BinInt.Z.pos_div_eucl p ten in + let acc0 = Concat (CamlStr (string_of_int (zTr r)), acc) in + match q with + | BinNums.Z0 -> acc0 + | BinNums.Zpos p0 -> string_of_pos p0 acc0 + | _ -> assert false + +(* +let string_of_Z_debug: BinNums.coq_Z -> pstring += fun p -> CamlStr (string_of_int (zTr p)) +*) + +let string_of_Z: BinNums.coq_Z -> pstring += function + | BinNums.Z0 -> CamlStr "0" + | BinNums.Zpos p -> string_of_pos p (CamlStr "") + | BinNums.Zneg p -> Concat (CamlStr "-", string_of_pos p (CamlStr "")) + +let timer ((f:'a -> 'b), (x:'a)) : 'b = + Gc.compact(); + let itime = (Unix.times()).Unix.tms_utime in + let r = f x in + let rt = (Unix.times()).Unix.tms_utime -. itime in + Printf.printf "time = %f\n" rt; + r diff --git a/lib/Impure/ocaml/ImpIOOracles.mli b/lib/Impure/ocaml/ImpIOOracles.mli new file mode 100644 index 00000000..6064286a --- /dev/null +++ b/lib/Impure/ocaml/ImpIOOracles.mli @@ -0,0 +1,33 @@ +open ImpPrelude + + +(* +Memoized version of translation from int -> BinNums.positive. +The first arg is an indicative bound on the max int translated: +it pre-computes all positives lower or equal to this bound. +*) +val memo_int2pos: int -> int -> BinNums.positive + +val read_line: unit -> pstring + +val print: pstring -> unit + +val println: pstring -> unit + +val string_of_Z: BinNums.coq_Z -> pstring + +val timer : (('a -> 'b ) * 'a) -> 'b + +val new_exit_observer: (unit -> unit) -> (unit -> unit) ref + +val set_exit_observer: (unit -> unit) ref * (unit -> unit) -> unit + +val exn2string: exn -> pstring + +val fail: pstring -> 'a + +exception ImpureFail of pstring;; + +val try_with_fail: (unit -> 'a) * (pstring -> exn -> 'a) -> 'a + +val try_with_any: (unit -> 'a) * (exn -> 'a) -> 'a diff --git a/lib/Impure/ocaml/ImpLoopOracles.ml b/lib/Impure/ocaml/ImpLoopOracles.ml new file mode 100644 index 00000000..cb7625e5 --- /dev/null +++ b/lib/Impure/ocaml/ImpLoopOracles.ml @@ -0,0 +1,78 @@ +open ImpPrelude +open Datatypes + +(** GENERIC ITERATIVE LOOP **) + +(* a simple version of loop *) +let simple_loop: ('a * ('a -> ('a, 'b) sum)) -> 'b + = fun (a0, f) -> + let rec iter: 'a -> 'b + = fun a -> + match f a with + | Coq_inl a' -> iter a' + | Coq_inr b -> b + in + iter a0;; + +(* loop from while *) +let while_loop: ('a * ('a -> ('a, 'b) sum)) -> 'b + = fun (a0, f) -> + let s = ref (f a0) in + while (match !s with Coq_inl _ -> true | _ -> false) do + match !s with + | Coq_inl a -> s:=f a + | _ -> assert false + done; + match !s with + | Coq_inr b -> b + | _ -> assert false;; + +let loop = simple_loop + + +(** GENERIC FIXPOINTS **) + +let std_rec (recf: ('a -> 'b ) -> 'a -> 'b): 'a -> 'b = + let rec f x = recf f x in + f + +let memo_rec (recf: ('a -> 'b ) -> 'a -> 'b): 'a -> 'b = + let memo = Hashtbl.create 10 in + let rec f x = + try + Hashtbl.find memo x + with + Not_found -> + let r = recf f x in + Hashtbl.replace memo x r; + r + in f + +let bare_rec (recf: ('a -> 'b ) -> 'a -> 'b): 'a -> 'b = + let fix = ref (fun x -> failwith "init") in + fix := (fun x -> recf !fix x); + !fix;; + +let buggy_rec (recf: ('a -> 'b ) -> 'a -> 'b): 'a -> 'b = + let memo = ref None in + let rec f x = + match !memo with + | Some y -> y + | None -> + let r = recf f x in + memo := Some r; + r + in f + +let xrec_mode = ref MemoRec + +let xrec_set_option : recMode -> unit += fun m -> xrec_mode := m + +let xrec : (('a -> 'b ) -> 'a -> 'b ) -> ('a -> 'b ) + = fun recf -> + match !xrec_mode with + | StdRec -> std_rec recf + | MemoRec -> memo_rec recf + | BareRec -> bare_rec recf + | BuggyRec -> buggy_rec recf diff --git a/lib/Impure/ocaml/ImpLoopOracles.mli b/lib/Impure/ocaml/ImpLoopOracles.mli new file mode 100644 index 00000000..194696a1 --- /dev/null +++ b/lib/Impure/ocaml/ImpLoopOracles.mli @@ -0,0 +1,8 @@ +open ImpPrelude +open Datatypes + +val loop: ('a * ('a -> ('a, 'b) sum)) -> 'b + +val xrec_set_option: recMode -> unit + +val xrec: (('a -> 'b ) -> 'a -> 'b ) -> ('a -> 'b ) diff --git a/lib/Integers.v b/lib/Integers.v index 68bff3a0..b6c41d8d 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -4,7 +4,7 @@ (* *) (* Xavier Leroy, INRIA Paris-Rocquencourt *) (* *) -(* Copyright Institut National de Recherche en Informatique et en *) +(* Copyright Institut National de Recherstestche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) (* under the terms of the GNU Lesser General Public License as *) (* published by the Free Software Foundation, either version 2.1 of *) @@ -17,8 +17,9 @@ (** Formalizations of machine integers modulo $2^N$ #2<sup>N</sup>#. *) Require Import Eqdep_dec Zquot Zwf. -Require Import Coqlib Zbits. +Require Import Coqlib Zbits Axioms. Require Archi. +Require Import Lia. (** * Comparisons *) @@ -30,6 +31,11 @@ Inductive comparison : Type := | Cgt : comparison (**r greater than *) | Cge : comparison. (**r greater than or equal *) +Definition comparison_eq: forall (x y: comparison), {x = y} + {x <> y}. +Proof. + decide equality. +Defined. + Definition negate_comparison (c: comparison): comparison := match c with | Ceq => Cne @@ -1190,6 +1196,34 @@ Proof. rewrite <- half_modulus_modulus. apply unsigned_range. Qed. +Local Transparent repr. +Lemma sign_bit_of_signed: forall x, + (testbit x (zwordsize - 1)) = lt x zero. +Proof. + intro. + rewrite sign_bit_of_unsigned. + unfold lt. + unfold signed, unsigned. + simpl. + pose proof half_modulus_pos as HMOD. + destruct (zlt 0 half_modulus) as [HMOD' | HMOD']. + 2: lia. + clear HMOD'. + destruct (zlt (intval x) half_modulus) as [ LOW | HIGH]. + { + destruct x as [ix RANGE]. + simpl in *. + destruct (zlt ix 0). lia. + reflexivity. + } + destruct (zlt _ _) as [LOW' | HIGH']; trivial. + destruct x as [ix RANGE]. + simpl in *. + rewrite half_modulus_modulus in *. + lia. +Qed. +Local Opaque repr. + Lemma bits_signed: forall x i, 0 <= i -> Z.testbit (signed x) i = testbit x (if zlt i zwordsize then i else zwordsize - 1). @@ -2423,6 +2457,57 @@ Proof. bit_solve. destruct (zlt (i + unsigned (sub iwordsize y)) zwordsize); auto. Qed. +Theorem shrx1_shr: + forall x, + ltu one (repr (zwordsize - 1)) = true -> + shrx x (repr 1) = shr (add x (shru x (repr (zwordsize - 1)))) (repr 1). +Proof. + intros. + rewrite shrx_shr by assumption. + rewrite shl_mul_two_p. + rewrite mul_commut. rewrite mul_one. + change (repr 1) with one. + rewrite unsigned_one. + change (two_p 1) with 2. + unfold sub. + rewrite unsigned_one. + assert (0 <= 2 <= max_unsigned). + { + unfold max_unsigned, modulus. + unfold zwordsize in *. + unfold ltu in *. + rewrite unsigned_one in H. + rewrite unsigned_repr in H. + { + destruct (zlt 1 (Z.of_nat wordsize - 1)) as [ LT | NONE]. + 2: discriminate. + clear H. + rewrite two_power_nat_two_p. + split. + lia. + set (w := (Z.of_nat wordsize)) in *. + assert ((two_p 2) <= (two_p w)) as MONO. + { + apply two_p_monotone. + lia. + } + change (two_p 2) with 4 in MONO. + lia. + } + generalize wordsize_max_unsigned. + fold zwordsize. + generalize wordsize_pos. + lia. + } + rewrite unsigned_repr by assumption. + simpl. + rewrite shru_lt_zero. + destruct (lt x zero). + reflexivity. + rewrite add_zero. + reflexivity. +Qed. + Theorem shrx_carry: forall x y, ltu y (repr (zwordsize - 1)) = true -> @@ -3701,6 +3786,103 @@ Proof. unfold ltu. apply zlt_true. change (unsigned z < 63). rewrite A; lia. Qed. +Lemma shr'63: + forall x, (shr' x (Int.repr 63)) = if lt x zero then mone else zero. +Proof. + intro. + unfold shr', mone, zero. + rewrite Int.unsigned_repr by (change Int.max_unsigned with 4294967295; lia). + apply same_bits_eq. + intros i BIT. + rewrite testbit_repr by assumption. + rewrite Z.shiftr_spec by lia. + rewrite bits_signed by lia. + simpl. + change zwordsize with 64 in *. + destruct (zlt _ _) as [LT | GE]. + { + replace i with 0 in * by lia. + change (0 + 63) with (zwordsize - 1). + rewrite sign_bit_of_signed. + destruct (lt x _). + all: rewrite testbit_repr by (change zwordsize with 64 in *; lia). + all: simpl; reflexivity. + } + change (64 - 1) with (zwordsize - 1). + rewrite sign_bit_of_signed. + destruct (lt x _). + all: rewrite testbit_repr by (change zwordsize with 64 in *; lia). + { symmetry. + apply Ztestbit_m1. + tauto. + } + symmetry. + apply Ztestbit_0. +Qed. + +Lemma shru'63: + forall x, (shru' x (Int.repr 63)) = if lt x zero then one else zero. +Proof. + intro. + unfold shru'. + rewrite Int.unsigned_repr by (change Int.max_unsigned with 4294967295; lia). + apply same_bits_eq. + intros i BIT. + rewrite testbit_repr by assumption. + rewrite Z.shiftr_spec by lia. + unfold lt. + rewrite signed_zero. + unfold one, zero. + destruct (zlt _ 0) as [LT | GE]. + { + rewrite testbit_repr by assumption. + destruct (zeq i 0) as [IZERO | INONZERO]. + { subst i. + change (Z.testbit (unsigned x) (0 + 63)) with (testbit x (zwordsize - 1)). + rewrite sign_bit_of_signed. + unfold lt. + rewrite signed_zero. + destruct (zlt _ _); try lia. + reflexivity. + } + change (Z.testbit (unsigned x) (i + 63)) with (testbit x (i+63)). + rewrite bits_above by (change zwordsize with 64; lia). + rewrite Ztestbit_1. + destruct (zeq i 0); trivial. + subst i. + lia. + } + destruct (zeq i 0) as [IZERO | INONZERO]. + { subst i. + change (Z.testbit (unsigned x) (0 + 63)) with (testbit x (zwordsize - 1)). + rewrite sign_bit_of_signed. + unfold lt. + rewrite signed_zero. + rewrite bits_zero. + destruct (zlt _ _); try lia; reflexivity. + } + change (Z.testbit (unsigned x) (i + 63)) with (testbit x (i + 63)). + rewrite bits_zero. + apply bits_above. + change zwordsize with 64. + lia. +Qed. + +Theorem shrx'1_shr': + forall x, + Int.ltu Int.one (Int.repr (zwordsize - 1)) = true -> + shrx' x (Int.repr 1) = shr' (add x (shru' x (Int.repr (Int64.zwordsize - 1)))) (Int.repr 1). +Proof. + intros. + rewrite shrx'_shr_2 by reflexivity. + change (Int.sub (Int.repr 64) (Int.repr 1)) with (Int.repr 63). + f_equal. f_equal. + rewrite shr'63. + rewrite shru'63. + rewrite shru'63. + destruct (lt x zero); reflexivity. +Qed. + Remark int_ltu_2_inv: forall y z, Int.ltu y iwordsize' = true -> @@ -4649,8 +4831,26 @@ End Int64. Strategy 0 [Wordsize_64.wordsize]. +Definition int_eq: forall (i1 i2: int), {i1=i2} + {i1<>i2}. +Proof. + generalize Z.eq_dec. intros. + destruct i1. destruct i2. generalize (H intval intval0). intro. + inversion H0. + - subst. left. assert (intrange = intrange0) by (apply proof_irr). congruence. + - right. intro. inversion H2. contradiction. +Qed. + Notation int64 := Int64.int. +Definition int64_eq: forall (i1 i2: int64), {i1=i2} + {i1<>i2}. +Proof. + generalize Z.eq_dec. intros. + destruct i1. destruct i2. generalize (H intval intval0). intro. + inversion H0. + - subst. left. assert (intrange = intrange0) by (apply proof_irr). congruence. + - right. intro. inversion H2. contradiction. +Qed. + Global Opaque Int.repr Int64.repr Byte.repr. (** * Specialization to offsets in pointer values *) @@ -4927,6 +5127,15 @@ Strategy 0 [Wordsize_Ptrofs.wordsize]. Notation ptrofs := Ptrofs.int. +Definition ptrofs_eq: forall (i1 i2: ptrofs), {i1=i2} + {i1<>i2}. +Proof. + generalize Z.eq_dec. intros. + destruct i1. destruct i2. generalize (H intval intval0). intro. + inversion H0. + - subst. left. assert (intrange = intrange0) by (apply proof_irr). congruence. + - right. intro. inversion H2. contradiction. +Qed. + Global Opaque Ptrofs.repr. Global Hint Resolve diff --git a/lib/IterList.v b/lib/IterList.v new file mode 100644 index 00000000..d28124c7 --- /dev/null +++ b/lib/IterList.v @@ -0,0 +1,112 @@ +Require Import Coqlib. +Require Import Lia. + +(** TODO: are these def and lemma already defined in the standard library ? + +In this case, it should be better to reuse those of the standard library ! + +*) + +Fixpoint iter {A} (n:nat) (f: A -> A) (x: A) {struct n}: A := + match n with + | O => x + | S n0 => iter n0 f (f x) + end. + +Lemma iter_S A (n:nat) (f: A -> A): forall x, iter (S n) f x = f (iter n f x). +Proof. + induction n; simpl; auto. + intros; erewrite <- IHn; simpl; auto. +Qed. + +Lemma iter_plus A (n m:nat) (f: A -> A): forall x, iter (n+m) f x = iter m f (iter n f x). +Proof. + induction n; simpl; auto. +Qed. + +Definition iter_tail {A} (n:nat) (l: list A) := iter n (@tl A) l. + +Lemma iter_tail_S {A} (n:nat) (l: list A): iter_tail (S n) l = tl (iter_tail n l). +Proof. + apply iter_S. +Qed. + +Lemma iter_tail_plus A (n m:nat) (l: list A): iter_tail (n+m) l = iter_tail m (iter_tail n l). +Proof. + apply iter_plus. +Qed. + +Lemma iter_tail_length A l1: forall (l2: list A), iter_tail (length l1) (l1 ++ l2) = l2. +Proof. + induction l1; auto. +Qed. + +Lemma iter_tail_nil A n: @iter_tail A n nil = nil. +Proof. + unfold iter_tail; induction n; simpl; auto. +Qed. + +Lemma iter_tail_reach_nil A (l: list A): iter_tail (length l) l = nil. +Proof. + rewrite (app_nil_end l) at 2. + rewrite iter_tail_length. + auto. +Qed. + +Lemma length_iter_tail {A} (n:nat): forall (l: list A), (n <= List.length l)%nat -> (List.length l = n + List.length (iter_tail n l))%nat. +Proof. + unfold iter_tail; induction n; auto. + intros l; destruct l. { simpl; lia. } + intros; simpl. erewrite IHn; eauto. + simpl in *; lia. +Qed. + +Lemma iter_tail_S_ex {A} (n:nat): forall (l: list A), (n < length l)%nat -> exists x, iter_tail n l = x::(iter_tail (S n) l). +Proof. + unfold iter_tail; induction n; simpl. + - intros l; destruct l; simpl; lia || eauto. + - intros l H; destruct (IHn (tl l)) as (x & H1). + + destruct l; simpl in *; try lia. + + rewrite H1; eauto. +Qed. + +Lemma iter_tail_inject1 {A} (n1 n2:nat) (l: list A): (n1 <= List.length l)%nat -> (n2 <= List.length l)%nat -> iter_tail n1 l = iter_tail n2 l -> n1=n2. +Proof. + intros H1 H2 EQ; exploit (length_iter_tail n1 l); eauto. + rewrite EQ. + rewrite (length_iter_tail n2 l); eauto. + lia. +Qed. + +Lemma iter_tail_nil_inject {A} (n:nat) (l: list A): iter_tail n l = nil -> (List.length l <= n)%nat. +Proof. + destruct (le_lt_dec n (List.length l)); try lia. + intros; exploit (iter_tail_inject1 n (length l) l); try lia. + rewrite iter_tail_reach_nil. auto. +Qed. + +Lemma list_length_z_nat (A: Type) (l: list A): list_length_z l = Z.of_nat (length l). +Proof. + induction l; auto. + rewrite list_length_z_cons. simpl. rewrite Zpos_P_of_succ_nat. lia. +Qed. + +Lemma list_length_nat_z (A: Type) (l: list A): length l = Z.to_nat (list_length_z l). +Proof. + intros; rewrite list_length_z_nat, Nat2Z.id. auto. +Qed. + +Lemma is_tail_list_nth_z A (l1 l2: list A): + is_tail l1 l2 -> list_nth_z l2 ((list_length_z l2) - (list_length_z l1)) = list_nth_z l1 0. +Proof. + induction 1; simpl. + - replace (list_length_z c - list_length_z c) with 0; lia || auto. + - assert (X: list_length_z (i :: c2) > list_length_z c1). + { rewrite !list_length_z_nat, <- Nat2Z.inj_gt. + exploit is_tail_bound; simpl; eauto. + lia. } + destruct (zeq (list_length_z (i :: c2) - list_length_z c1) 0) as [Y|Y]; try lia. + replace (Z.pred (list_length_z (i :: c2) - list_length_z c1)) with (list_length_z c2 - list_length_z c1); auto. + rewrite list_length_z_cons. + lia. +Qed. diff --git a/lib/Lattice.v b/lib/Lattice.v index aea331a0..99a31632 100644 --- a/lib/Lattice.v +++ b/lib/Lattice.v @@ -32,7 +32,8 @@ Local Unset Case Analysis Schemes. [bot], and an upper bound operation [lub]. Note that we do not demand that [lub] computes the least upper bound. *) -Module Type SEMILATTICE. + +Module Type SEMILATTICE_WITHOUT_BOTTOM. Parameter t: Type. Parameter eq: t -> t -> Prop. @@ -44,25 +45,124 @@ Module Type SEMILATTICE. Parameter ge: t -> t -> Prop. Axiom ge_refl: forall x y, eq x y -> ge x y. Axiom ge_trans: forall x y z, ge x y -> ge y z -> ge x z. - Parameter bot: t. - Axiom ge_bot: forall x, ge x bot. Parameter lub: t -> t -> t. Axiom ge_lub_left: forall x y, ge (lub x y) x. Axiom ge_lub_right: forall x y, ge (lub x y) y. +End SEMILATTICE_WITHOUT_BOTTOM. + +Module Type SEMILATTICE. + Include SEMILATTICE_WITHOUT_BOTTOM. + Parameter bot: t. + Axiom ge_bot: forall x, ge x bot. End SEMILATTICE. (** A semi-lattice ``with top'' is similar, but also has a greatest element [top]. *) Module Type SEMILATTICE_WITH_TOP. - Include SEMILATTICE. Parameter top: t. Axiom ge_top: forall x, ge top x. - End SEMILATTICE_WITH_TOP. + +Module ADD_BOTTOM(L : SEMILATTICE_WITHOUT_BOTTOM) <: SEMILATTICE. + Definition t := option L.t. + Definition eq (a b : t) := + match a, b with + | None, None => True + | Some x, Some y => L.eq x y + | Some _, None | None, Some _ => False + end. + + Lemma eq_refl: forall x, eq x x. + Proof. + unfold eq; destruct x; trivial. + apply L.eq_refl. + Qed. + + Lemma eq_sym: forall x y, eq x y -> eq y x. + Proof. + unfold eq; destruct x; destruct y; trivial. + apply L.eq_sym. + Qed. + + Lemma eq_trans: forall x y z, eq x y -> eq y z -> eq x z. + Proof. + unfold eq; destruct x; destruct y; destruct z; trivial. + - apply L.eq_trans. + - contradiction. + Qed. + + Definition beq (x y : t) := + match x, y with + | None, None => true + | Some x, Some y => L.beq x y + | Some _, None | None, Some _ => false + end. + + Lemma beq_correct: forall x y, beq x y = true -> eq x y. + Proof. + unfold beq, eq. + destruct x; destruct y; trivial; try congruence. + apply L.beq_correct. + Qed. + + Definition ge (x y : t) := + match x, y with + | None, Some _ => False + | _, None => True + | Some a, Some b => L.ge a b + end. + + Lemma ge_refl: forall x y, eq x y -> ge x y. + Proof. + unfold eq, ge. + destruct x; destruct y; trivial. + apply L.ge_refl. + Qed. + + Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. + Proof. + unfold ge. + destruct x; destruct y; destruct z; trivial; try contradiction. + apply L.ge_trans. + Qed. + + Definition bot: t := None. + Lemma ge_bot: forall x, ge x bot. + Proof. + unfold ge, bot. + destruct x; trivial. + Qed. + + Definition lub (a b : t) := + match a, b with + | None, _ => b + | _, None => a + | (Some x), (Some y) => Some (L.lub x y) + end. + + Lemma ge_lub_left: forall x y, ge (lub x y) x. + Proof. + unfold ge, lub. + destruct x; destruct y; trivial. + - apply L.ge_lub_left. + - apply L.ge_refl. + apply L.eq_refl. + Qed. + + Lemma ge_lub_right: forall x y, ge (lub x y) y. + Proof. + unfold ge, lub. + destruct x; destruct y; trivial. + - apply L.ge_lub_right. + - apply L.ge_refl. + apply L.eq_refl. + Qed. +End ADD_BOTTOM. + (** * Semi-lattice over maps *) Set Implicit Arguments. @@ -1224,11 +1224,56 @@ Module PTree <: TREE. apply fold1'_xelements' with (l := @nil (positive * A)). Qed. + Local Open Scope positive. + Lemma set_disjoint1: + forall (A: Type)(i d : elt) (m: t A) (x y: A), + set (i + d) y (set i x m) = set i x (set (i + d) y m). + Proof. + intros. + apply extensionality. + intro j. + destruct (peq j i) as [EQ_i_j | NEQ_j_i]. + - subst i. + rewrite gss. + rewrite gso by lia. + apply gss. + - rewrite (gso _ _ NEQ_j_i). + destruct (peq j (i + d)) as [EQ | NEQ]. + + subst j. + rewrite gss. + rewrite gss. + reflexivity. + + rewrite (gso _ _ NEQ). + rewrite (gso _ _ NEQ). + apply (gso _ _ NEQ_j_i). + Qed. + + Local Open Scope positive. + Lemma set_disjoint: + forall (A: Type)(i j : elt) (m: t A) (x y: A), + i <> j -> + set j y (set i x m) = set i x (set j y m). + Proof. + intros. + destruct (Pos.compare_spec i j) as [Heq | Hlt | Hlt]. + { congruence. } + { + rewrite (Pos.lt_iff_add i j) in Hlt. + destruct Hlt as [d Hd]. + subst j. + apply set_disjoint1. + } + rewrite (Pos.lt_iff_add j i) in Hlt. + destruct Hlt as [d Hd]. + subst i. + symmetry. + apply set_disjoint1. + Qed. + Arguments empty A : simpl never. Arguments get {A} p m : simpl never. Arguments set {A} p x m : simpl never. Arguments remove {A} p m : simpl never. - End PTree. (** * An implementation of maps over type [positive] *) @@ -1306,6 +1351,15 @@ Module PMap <: MAP. intros. unfold set. simpl. decEq. apply PTree.set2. Qed. + Local Open Scope positive. + Lemma set_disjoint: + forall (A: Type) (i j : elt) (x y: A) (m: t A), + i <> j -> + set j y (set i x m) = set i x (set j y m). + Proof. + intros. unfold set. decEq. apply PTree.set_disjoint. assumption. + Qed. + End PMap. (** * An implementation of maps over any type that injects into type [positive] *) @@ -1373,6 +1427,16 @@ Module IMap(X: INDEXED_TYPE). intros. unfold set. apply PMap.set2. Qed. + Lemma set_disjoint: + forall (A: Type) (i j : elt) (x y: A) (m: t A), + i <> j -> + set j y (set i x m) = set i x (set j y m). + Proof. + intros. unfold set. apply PMap.set_disjoint. + intro INEQ. + assert (i = j) by (apply X.index_inj; auto). + auto. + Qed. End IMap. Module ZIndexed. diff --git a/lib/OptionMonad.v b/lib/OptionMonad.v new file mode 100644 index 00000000..f3566d5c --- /dev/null +++ b/lib/OptionMonad.v @@ -0,0 +1,76 @@ +(* Declare Scope option_monad_scope. *) + +Notation "'SOME' X <- A 'IN' B" := (match A with Some X => B | None => None end) + (at level 200, X ident, A at level 100, B at level 200) + : option_monad_scope. + +Notation "'ASSERT' A 'IN' B" := (if A then B else None) + (at level 200, A at level 100, B at level 200) + : option_monad_scope. + +Local Open Scope option_monad_scope. + + +(** Simple tactics for option-monad *) + +Ltac deepest_match exp := + match exp with + | context f [match ?expr with | _ => _ end] => ltac: (deepest_match expr) + | _ => exp + end. + +Ltac autodestruct := + let EQ := fresh "EQ" in + match goal with + | |- context f [match ?expr with | _ => _ end] => + let t := ltac: (deepest_match expr) in + destruct t eqn:EQ; generalize EQ; clear EQ; congruence || trivial + end. + +(* deprecated version of "autodestruct". the new one seems a better replacement +Ltac dummy_autodestruct := + let EQ := fresh "EQ" in + match goal with + | |- context f [match ?expr with | _ => _ end] => destruct expr eqn:EQ; generalize EQ; clear EQ; congruence || trivial + end. +*) + +Lemma destruct_SOME A B (P: option B -> Prop) (e: option A) (f: A -> option B): + (forall x, e = Some x -> P (f x)) -> (e = None -> P None) -> (P (SOME x <- e IN f x)). +Proof. + intros; destruct e; simpl; auto. +Qed. + +Lemma destruct_ASSERT B (P: option B -> Prop) (e: bool) (x: option B): + (e = true -> P x) -> (e = false -> P None) -> (P (ASSERT e IN x)). +Proof. + intros; destruct e; simpl; auto. +Qed. + +Ltac inversion_SOME x := + try (eapply destruct_SOME; [ let x := fresh x in intro x | simpl; try congruence ]). + +Ltac inversion_ASSERT := + try (eapply destruct_ASSERT; [ idtac | simpl; try congruence ]). + +Ltac simplify_someHyp := + match goal with + | H: None = Some _ |- _ => inversion H; clear H; subst + | H: Some _ = None |- _ => inversion H; clear H; subst + | H: ?t = ?t |- _ => clear H + | H: Some _ = Some _ |- _ => inversion H; clear H; subst + | H: Some _ <> None |- _ => clear H + | H: None <> Some _ |- _ => clear H + | H: _ = Some _ |- _ => (try rewrite !H in * |- *); generalize H; clear H + | H: _ = None |- _ => (try rewrite !H in * |- *); generalize H; clear H + | H: None = _ |- _ => (try rewrite <- !H in * |- *); generalize H; clear H + end. + +Ltac simplify_someHyps := + repeat (simplify_someHyp; simpl in * |- *). + +Ltac try_simplify_someHyps := + try (intros; simplify_someHyps; eauto). + +Ltac simplify_option := repeat (try_simplify_someHyps; autodestruct); try_simplify_someHyps. + diff --git a/lib/UnionFind.v b/lib/UnionFind.v index 1bc2f657..1c37a35b 100644 --- a/lib/UnionFind.v +++ b/lib/UnionFind.v @@ -126,6 +126,15 @@ Module Type UNIONFIND. pathlen uf x + pathlen uf b + 1 else pathlen uf x. + Axiom pathlen_union: + forall uf a b x, + pathlen (union uf a b) x = + if elt_eq (repr uf a) (repr uf b) then + pathlen uf x + else if elt_eq (repr uf x) (repr uf a) then + (pathlen uf x)+1 + else + (pathlen uf x). Axiom pathlen_gt_merge: forall uf a b x y, repr uf x = repr uf y -> @@ -533,6 +542,7 @@ Qed. End PATHLEN. + (* Path length and merge *) Lemma pathlen_merge: @@ -551,16 +561,49 @@ Proof. set (uf' := identify uf (repr uf a) b (repr_res_none uf a) (not_eq_sym n)). pattern x. apply (well_founded_ind (mwf uf')); intros. rewrite (pathlen_unroll uf'). destruct (M.get x0 (m uf')) as [x'|] eqn:G. - rewrite H; auto. simpl in G. rewrite M.gsspec in G. - destruct (M.elt_eq x0 (repr uf a)). rewrite e. rewrite repr_canonical. rewrite dec_eq_true. - inversion G. subst x'. rewrite dec_eq_false; auto. - replace (pathlen uf (repr uf a)) with 0. lia. - symmetry. apply pathlen_none. apply repr_res_none. - rewrite (repr_unroll uf x0), (pathlen_unroll uf x0); rewrite G. - destruct (M.elt_eq (repr uf x') (repr uf a)); lia. - simpl in G. rewrite M.gsspec in G. destruct (M.elt_eq x0 (repr uf a)); try discriminate. - rewrite (repr_none uf x0) by auto. rewrite dec_eq_false; auto. - symmetry. apply pathlen_zero; auto. apply repr_none; auto. + + rewrite H; auto. clear H. simpl in G. rewrite M.gsspec in G. + destruct (M.elt_eq x0 (repr uf a)). + - rewrite e, repr_canonical, dec_eq_true. + inversion G. subst x'. rewrite dec_eq_false; auto. + replace (pathlen uf (repr uf a)) with 0; try lia. + symmetry. apply pathlen_none. apply repr_res_none. + - rewrite (repr_unroll uf x0), (pathlen_unroll uf x0), G. + destruct (M.elt_eq (repr uf x') (repr uf a)); lia. + + clear H; simpl in G. rewrite M.gsspec in G. destruct (M.elt_eq x0 (repr uf a)); try discriminate. + rewrite (repr_none uf x0) by auto. rewrite dec_eq_false; auto. + symmetry. apply pathlen_zero; auto. apply repr_none; auto. +Qed. + +Lemma pathlen_union: + forall uf a b x, + pathlen (union uf a b) x = + if M.elt_eq (repr uf a) (repr uf b) then + pathlen uf x + else if M.elt_eq (repr uf x) (repr uf a) then + (pathlen uf x)+1 + else + (pathlen uf x). +Proof. + intros. unfold union. + destruct (M.elt_eq (repr uf a) (repr uf b)). + auto. + set (uf' := identify uf _ _ _ _). + assert (LENa: pathlen uf (repr uf a) = 0). + { apply pathlen_none. apply repr_res_none. } + pattern x. apply (well_founded_ind (mwf uf')); intros. + rewrite (pathlen_unroll uf'). destruct (M.get x0 (m uf')) as [x'|] eqn:G. + + rewrite H; auto. clear H. simpl in G. rewrite M.gsspec in G. + destruct (M.elt_eq x0 (repr uf a)). + - inversion G; clear G. subst. + rewrite !repr_canonical, dec_eq_true. + rewrite dec_eq_false; auto. + rewrite LENa. rewrite (pathlen_none uf (repr uf b)); try lia. + apply repr_res_none. + - rewrite (repr_unroll uf x0), G, ! (pathlen_some _ _ _ G). + destruct (M.elt_eq _ _); auto. + + clear H. simpl in G. rewrite M.gsspec in G. + destruct (M.elt_eq _ (repr uf a)); try discriminate. + rewrite (repr_none _ _ G), !(pathlen_none _ _ G), dec_eq_false; auto. Qed. Lemma pathlen_gt_merge: diff --git a/lib/extra/HashedMap.v b/lib/extra/HashedMap.v new file mode 100644 index 00000000..a7d6f589 --- /dev/null +++ b/lib/extra/HashedMap.v @@ -0,0 +1,460 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* David Monniaux CNRS, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + +Require Import ZArith. +Require Import Bool. +Require Import List. +Require Coq.Logic.Eqdep_dec. + +(* begin from Maps *) +Fixpoint prev_append (i j: positive) {struct i} : positive := + match i with + | xH => j + | xI i' => prev_append i' (xI j) + | xO i' => prev_append i' (xO j) + end. + +Definition prev (i: positive) : positive := + prev_append i xH. + +Lemma prev_append_prev i j: + prev (prev_append i j) = prev_append j i. +Proof. + revert j. unfold prev. + induction i as [i IH|i IH|]. 3: reflexivity. + intros j. simpl. rewrite IH. reflexivity. + intros j. simpl. rewrite IH. reflexivity. +Qed. + +Lemma prev_involutive i : + prev (prev i) = i. +Proof (prev_append_prev i xH). + +Lemma prev_append_inj i j j' : + prev_append i j = prev_append i j' -> j = j'. +Proof. + revert j j'. + induction i as [i Hi|i Hi|]; intros j j' H; auto; + specialize (Hi _ _ H); congruence. +Qed. + +(* end from Maps *) + +Lemma orb_idem: forall b, orb b b = b. +Proof. + destruct b; reflexivity. +Qed. + +Lemma andb_idem: forall b, andb b b = b. +Proof. + destruct b; reflexivity. +Qed. + +Lemma andb_negb_false: forall b, andb b (negb b) = false. +Proof. + destruct b; reflexivity. +Qed. + +Hint Rewrite orb_false_r andb_false_r andb_true_r orb_true_r orb_idem andb_idem andb_negb_false : pmap. + +Parameter T : Type. +Parameter T_eq_dec : forall (x y : T), {x = y} + {x <> y}. + +Inductive pmap : Type := +| Empty : pmap +| Node : pmap -> option T -> pmap -> pmap. +Definition empty := Empty. + +Definition is_empty x := + match x with + | Empty => true + | Node _ _ _ => false + end. + +Definition is_some (x : option T) := + match x with + | Some _ => true + | None => false + end. + +Fixpoint wf x := + match x with + | Empty => true + | Node b0 f b1 => + (wf b0) && (wf b1) && + ((negb (is_empty b0)) || (is_some f) || (negb (is_empty b1))) + end. + +Definition iswf x := (wf x)=true. + +Lemma empty_wf : iswf empty. +Proof. + reflexivity. +Qed. + +Definition pmap_eq : + forall s s': pmap, { s=s' } + { s <> s' }. +Proof. + generalize T_eq_dec. + induction s; destruct s'; repeat decide equality. +Qed. + +Fixpoint get (i : positive) (s : pmap) {struct i} : option T := + match s with + | Empty => None + | Node b0 f b1 => + match i with + | xH => f + | xO ii => get ii b0 + | xI ii => get ii b1 + end + end. + +Lemma gempty : + forall i : positive, + get i Empty = None. +Proof. + destruct i; simpl; reflexivity. +Qed. + +Hint Resolve gempty : pmap. +Hint Rewrite gempty : pmap. + +Definition node (b0 : pmap) (f : option T) (b1 : pmap) : pmap := + match b0, f, b1 with + | Empty, None, Empty => Empty + | _, _, _ => Node b0 f b1 + end. + +Lemma wf_node : + forall b0 f b1, + iswf b0 -> iswf b1 -> iswf (node b0 f b1). +Proof. + destruct b0; destruct f; destruct b1; simpl. + all: unfold iswf; simpl; intros; trivial. + all: autorewrite with pmap; trivial. + all: rewrite H. + all: rewrite H0. + all: reflexivity. +Qed. + +Hint Resolve wf_node: pmap. + +Lemma gnode : + forall b0 f b1 i, + get i (node b0 f b1) = + get i (Node b0 f b1). +Proof. + destruct b0; simpl; trivial. + destruct f; simpl; trivial. + destruct b1; simpl; trivial. + intro. + rewrite gempty. + destruct i; simpl; trivial. + all: symmetry; apply gempty. +Qed. + +Hint Rewrite gnode : pmap. + +Fixpoint set (i : positive) (j : T) (s : pmap) {struct i} : pmap := + match s with + | Empty => + match i with + | xH => Node Empty (Some j) Empty + | xO ii => Node (set ii j Empty) None Empty + | xI ii => Node Empty None (set ii j Empty) + end + | Node b0 f b1 => + match i with + | xH => Node b0 (Some j) b1 + | xO ii => Node (set ii j b0) f b1 + | xI ii => Node b0 f (set ii j b1) + end + end. + +Lemma set_nonempty: + forall i j s, is_empty (set i j s) = false. +Proof. + induction i; destruct s; simpl; trivial. +Qed. + +Hint Rewrite set_nonempty : pmap. +Hint Resolve set_nonempty : pmap. + +Lemma wf_set: + forall i j s, (iswf s) -> (iswf (set i j s)). +Proof. + induction i; destruct s; simpl; trivial. + all: unfold iswf in *; simpl. + all: autorewrite with pmap; simpl; trivial. + 1,3: auto with pmap. + all: intro Z. + all: repeat rewrite andb_true_iff in Z. + all: intuition. +Qed. + +Hint Resolve wf_set : pset. + +Theorem gss : + forall (i : positive) (j : T) (s : pmap), + get i (set i j s) = Some j. +Proof. + induction i; destruct s; simpl; auto. +Qed. + +Hint Resolve gss : pmap. +Hint Rewrite gss : pmap. + +Theorem gso : + forall (i j : positive) (k : T) (s : pmap), + i <> j -> + get j (set i k s) = get j s. +Proof. + induction i; destruct j; destruct s; simpl; intro; auto with pmap. + 5, 6: congruence. + all: rewrite IHi by congruence. + all: trivial. + all: apply gempty. +Qed. + +Hint Resolve gso : pmap. + +Fixpoint remove (i : positive) (s : pmap) { struct i } : pmap := + match i with + | xH => + match s with + | Empty => Empty + | Node b0 f b1 => node b0 None b1 + end + | xO ii => + match s with + | Empty => Empty + | Node b0 f b1 => node (remove ii b0) f b1 + end + | xI ii => + match s with + | Empty => Empty + | Node b0 f b1 => node b0 f (remove ii b1) + end + end. + +Lemma wf_remove : + forall i s, (iswf s) -> (iswf (remove i s)). +Proof. + induction i; destruct s; simpl; trivial. + all: unfold iswf in *; simpl. + all: intro Z. + all: repeat rewrite andb_true_iff in Z. + all: apply wf_node. + all: intuition. + all: apply IHi. + all: assumption. +Qed. + +Fixpoint remove_noncanon (i : positive) (s : pmap) { struct i } : pmap := + match i with + | xH => + match s with + | Empty => Empty + | Node b0 f b1 => Node b0 None b1 + end + | xO ii => + match s with + | Empty => Empty + | Node b0 f b1 => Node (remove_noncanon ii b0) f b1 + end + | xI ii => + match s with + | Empty => Empty + | Node b0 f b1 => Node b0 f (remove_noncanon ii b1) + end + end. + +Lemma remove_noncanon_same: + forall i j s, (get j (remove i s)) = (get j (remove_noncanon i s)). +Proof. + induction i; destruct s; simpl; trivial. + all: rewrite gnode. + 3: reflexivity. + all: destruct j; simpl; trivial. +Qed. + +Lemma remove_empty : + forall i, remove i Empty = Empty. +Proof. + induction i; simpl; trivial. +Qed. + +Hint Rewrite remove_empty : pmap. +Hint Resolve remove_empty : pmap. + +Lemma gremove_noncanon_s : + forall i : positive, + forall s : pmap, + get i (remove_noncanon i s) = None. +Proof. + induction i; destruct s; simpl; trivial. +Qed. + +Theorem grs : + forall i : positive, + forall s : pmap, + get i (remove i s) = None. +Proof. + intros. + rewrite remove_noncanon_same. + apply gremove_noncanon_s. +Qed. + +Hint Resolve grs : pmap. +Hint Rewrite grs : pmap. + +Lemma gremove_noncanon_o : + forall i j : positive, + forall s : pmap, + i<>j -> + get j (remove_noncanon i s) = get j s. +Proof. + induction i; destruct j; destruct s; simpl; intro; trivial. + 1, 2: rewrite IHi by congruence. + 1, 2: reflexivity. + congruence. +Qed. + +Theorem gro : + forall (i j : positive) (s : pmap), + i<>j -> + get j (remove i s) = get j s. +Proof. + intros. + rewrite remove_noncanon_same. + apply gremove_noncanon_o. + assumption. +Qed. + +Hint Resolve gro : pmap. + +Section MAP2. + + Variable f : option T -> option T -> option T. + + Section NONE_NONE. + Hypothesis f_none_none : f None None = None. + + Fixpoint map2_Empty (b : pmap) := + match b with + | Empty => Empty + | Node b0 bf b1 => + node (map2_Empty b0) (f None bf) (map2_Empty b1) + end. + + Lemma gmap2_Empty: forall i b, + get i (map2_Empty b) = f None (get i b). + Proof. + induction i; destruct b as [ | b0 bf b1]; intros; simpl in *. + all: try congruence. + - replace + (match node (map2_Empty b0) (f None bf) (map2_Empty b1) with + | Empty => None + | Node _ _ c1 => get i c1 + end) + with (get (xI i) (node (map2_Empty b0) (f None bf) (map2_Empty b1))). + + rewrite gnode. + simpl. apply IHi. + + destruct node; auto with pmap. + - replace + (match node (map2_Empty b0) (f None bf) (map2_Empty b1) with + | Empty => None + | Node c0 _ _ => get i c0 + end) + with (get (xO i) (node (map2_Empty b0) (f None bf) (map2_Empty b1))). + + rewrite gnode. + simpl. apply IHi. + + destruct node; auto with pmap. + - change (match node (map2_Empty b0) (f None bf) (map2_Empty b1) with + | Empty => None + | Node _ cf _ => cf + end) with (get xH (node (map2_Empty b0) (f None bf) (map2_Empty b1))). + rewrite gnode. reflexivity. + Qed. + + Fixpoint map2 (a b : pmap) := + match a with + | Empty => map2_Empty b + | (Node a0 af a1) => + match b with + | (Node b0 bf b1) => + node (map2 a0 b0) (f af bf) (map2 a1 b1) + | Empty => + node (map2 a0 Empty) (f af None) (map2 a1 Empty) + end + end. + + Lemma gmap2: forall a b i, + get i (map2 a b) = f (get i a) (get i b). + Proof. + induction a as [ | a0 IHa0 af a1 IHa1]; intros; simpl. + { rewrite gmap2_Empty. + rewrite gempty. + reflexivity. } + destruct b as [ | b0 bf b1 ]; simpl; rewrite gnode. + - destruct i; simpl. + + rewrite IHa1. rewrite gempty. + reflexivity. + + rewrite IHa0. rewrite gempty. + reflexivity. + + reflexivity. + - destruct i; simpl; congruence. + Qed. + End NONE_NONE. + + Section IDEM. + Hypothesis f_idem : forall x, f x x = x. + + Fixpoint map2_idem (a b : pmap) := + if pmap_eq a b then a else + match a with + | Empty => map2_Empty b + | (Node a0 af a1) => + match b with + | (Node b0 bf b1) => + node (map2_idem a0 b0) (f af bf) (map2_idem a1 b1) + | Empty => + node (map2_idem a0 Empty) (f af None) (map2_idem a1 Empty) + end + end. + + Lemma gmap2_idem: forall a b i, + get i (map2_idem a b) = f (get i a) (get i b). + Proof. + induction a as [ | a0 IHa0 af a1 IHa1]; intros; simpl. + { destruct pmap_eq. + - subst b. rewrite gempty. congruence. + - rewrite gempty. + rewrite gmap2_Empty by congruence. + reflexivity. + } + destruct pmap_eq. + { subst b. + congruence. + } + destruct b as [ | b0 bf b1 ]; simpl; rewrite gnode. + - destruct i; simpl. + + rewrite IHa1. rewrite gempty. + reflexivity. + + rewrite IHa0. rewrite gempty. + reflexivity. + + reflexivity. + - destruct i; simpl; congruence. + Qed. + End IDEM. +End MAP2. |