text:
(** * MoreInd: More on Induction *)

Require Export "ProofObjects".

(* ##################################################### *)
(** * Induction Principles *)

(** This is a good point to pause and take a deeper look at induction
    principles.

    Every time we declare a new [Inductive] datatype, Coq
    automatically generates and proves an _induction principle_
    for this type.

    The induction principle for a type [t] is called [t_ind].  Here is
    the one for natural numbers: *)

Check nat_ind.
(*  ===> nat_ind :
           forall P : nat -> Prop,
              P 0  ->
              (forall n : nat, P n -> P (S n))  ->
              forall n : nat, P n  *)

(** *** *)
(** The [induction] tactic is a straightforward wrapper that, at
    its core, simply performs [apply t_ind].  To see this more
    clearly, let's experiment a little with using [apply nat_ind]
    directly, instead of the [induction] tactic, to carry out some
    proofs.  Here, for example, is an alternate proof of a theorem
    that we saw in the [Basics] chapter. *)

Theorem mult_0_r' : forall n:nat,
  n * 0 = 0.
Proof.
  apply nat_ind.
  - (* O *) reflexivity.
  - (* S *) simpl. intros n IHn. rewrite -> IHn.
    reflexivity.  Qed.

(** This proof is basically the same as the earlier one, but a
    few minor differences are worth noting.  First, in the induction
    step of the proof (the ["S"] case), we have to do a little
    bookkeeping manually (the [intros]) that [induction] does
    automatically.

    Second, we do not introduce [n] into the context before applying
    [nat_ind] -- the conclusion of [nat_ind] is a quantified formula,
    and [apply] needs this conclusion to exactly match the shape of
    the goal state, including the quantifier.  The [induction] tactic
    works either with a variable in the context or a quantified
    variable in the goal.

    Third, the [apply] tactic automatically chooses variable names for
    us (in the second subgoal, here), whereas [induction] lets us
    specify (with the [as...]  clause) what names should be used.  The
    automatic choice is actually a little unfortunate, since it
    re-uses the name [n] for a variable that is different from the [n]
    in the original theorem.  This is we have labeled the second
    subgoal just [S] -- if we tried to write it out in the more
    explicit form that we've been using for most proofs, we'd have to
    write [n = S n], which doesn't make a lot of sense!  All of these
    conveniences make [induction] nicer to use in practice than
    applying induction principles like [nat_ind] directly.  But it is
    important to realize that, modulo this little bit of bookkeeping,
    applying [nat_ind] is what we are really doing. *)

(** **** Exercise: 2 stars, optional (plus_one_r')  *)
(** Complete this proof as we did [mult_0_r'] above, without using
    the [induction] tactic. *)

Theorem plus_one_r' : forall n:nat,
  n + 1 = S n.
Proof.
  apply nat_ind.
  - simpl. reflexivity.
  - intros. simpl.  rewrite H. reflexivity.
Qed.
(** [] *)

(** Coq generates induction principles for every datatype defined with
    [Inductive], including those that aren't recursive. (Although
    we don't need induction to prove properties of non-recursive
    datatypes, the idea of an induction principle still makes sense
    for them: it gives a way to prove that a property holds for all
    values of the type.)

    These generated principles follow a similar pattern. If we define a
    type [t] with constructors [c1] ... [cn], Coq generates a theorem
    with this shape:
    t_ind :
       forall P : t -> Prop,
            ... case for c1 ... ->
            ... case for c2 ... ->
            ...
            ... case for cn ... ->
            forall n : t, P n
    The specific shape of each case depends on the arguments to the
    corresponding constructor.  Before trying to write down a general
    rule, let's look at some more examples. First, an example where
    the constructors take no arguments: *)

Inductive yesno : Type :=
  | yes : yesno
  | no : yesno.

Check yesno_ind.
(* ===> yesno_ind : forall P : yesno -> Prop,
                      P yes  ->
                      P no  ->
                      forall y : yesno, P y *)

(** **** Exercise: 1 star, optional (rgb)  *)
(** Write out the induction principle that Coq will generate for the
    following datatype.  Write down your answer on paper or type it
    into a comment, and then compare it with what Coq prints. *)

Inductive rgb : Type :=
  | red : rgb
  | green : rgb
  | blue : rgb.
Check rgb_ind.
(** [] *)

(** Here's another example, this time with one of the constructors
    taking some arguments. *)

Inductive natlist : Type :=
  | nnil : natlist
  | ncons : nat -> natlist -> natlist.

Check natlist_ind.
(* ===> (modulo a little variable renaming for clarity)
   natlist_ind :
      forall P : natlist -> Prop,
         P nnil  ->
         (forall (n : nat) (l : natlist), P l -> P (ncons n l)) ->
         forall n : natlist, P n *)

(** **** Exercise: 1 star, optional (natlist1)  *)
(** Suppose we had written the above definition a little
   differently: *)

Inductive natlist1 : Type :=
  | nnil1 : natlist1
  | nsnoc1 : natlist1 -> nat -> natlist1.

(** Now what will the induction principle look like? *)
(** [] *)

(** From these examples, we can extract this general rule:

    - The type declaration gives several constructors; each
      corresponds to one clause of the induction principle.
    - Each constructor [c] takes argument types [a1]...[an].
    - Each [ai] can be either [t] (the datatype we are defining) or
      some other type [s].
    - The corresponding case of the induction principle
      says (in English):
        - "for all values [x1]...[xn] of types [a1]...[an], if [P]
           holds for each of the inductive arguments (each [xi] of
           type [t]), then [P] holds for [c x1 ... xn]".

*)

(** **** Exercise: 1 star, optional (byntree_ind)  *)
(** Write out the induction principle that Coq will generate for the
    following datatype.  Write down your answer on paper or type it
    into a comment, and then compare it with what Coq prints. *)

Inductive byntree : Type :=
 | bempty : byntree
 | bleaf  : yesno -> byntree
 | nbranch : yesno -> byntree -> byntree -> byntree.
(** [] *)

(** **** Exercise: 1 star, optional (ex_set)  *)
(** Here is an induction principle for an inductively defined
    set.
      ExSet_ind :
         forall P : ExSet -> Prop,
             (forall b : bool, P (con1 b)) ->
             (forall (n : nat) (e : ExSet), P e -> P (con2 n e)) ->
             forall e : ExSet, P e
    Give an [Inductive] definition of [ExSet]: *)

Inductive ExSet : Type :=
  | con1 : bool -> ExSet
  | con2 : nat -> ExSet -> ExSet
.

(** [] *)

(** What about polymorphic datatypes?

    The inductive definition of polymorphic lists
      Inductive list (X:Type) : Type :=
        | nil : list X
        | cons : X -> list X -> list X.
    is very similar to that of [natlist].  The main difference is
    that, here, the whole definition is _parameterized_ on a set [X]:
    that is, we are defining a _family_ of inductive types [list X],
    one for each [X].  (Note that, wherever [list] appears in the body
    of the declaration, it is always applied to the parameter [X].)
    The induction principle is likewise parameterized on [X]:
     list_ind :
       forall (X : Type) (P : list X -> Prop),
          P [] ->
          (forall (x : X) (l : list X), P l -> P (x :: l)) ->
          forall l : list X, P l
    Note the wording here (and, accordingly, the form of [list_ind]):
    The _whole_ induction principle is parameterized on [X].  That is,
    [list_ind] can be thought of as a polymorphic function that, when
    applied to a type [X], gives us back an induction principle
    specialized to the type [list X]. *)

(** **** Exercise: 1 star, optional (tree)  *)
(** Write out the induction principle that Coq will generate for
   the following datatype.  Compare your answer with what Coq
   prints. *)

Inductive tree (X:Type) : Type :=
  | leaf : X -> tree X
  | node : tree X -> tree X -> tree X.
Check tree_ind.
(** [] *)

(** **** Exercise: 1 star, optional (mytype)  *)
(** Find an inductive definition that gives rise to the
    following induction principle:
      mytype_ind :
        forall (X : Type) (P : mytype X -> Prop),
            (forall x : X, P (constr1 X x)) ->
            (forall n : nat, P (constr2 X n)) ->
            (forall m : mytype X, P m ->
               forall n : nat, P (constr3 X m n)) ->
            forall m : mytype X, P m
*)
Inductive mytype (X:Type) : Type :=
  | constr1 : X -> mytype X
  | constr2 : nat -> mytype X
  | constr3 : mytype X -> nat -> mytype X
.

Check mytype_ind.
(** **** Exercise: 1 star, optional (foo)  *)
(** Find an inductive definition that gives rise to the
    following induction principle:
      foo_ind :
        forall (X Y : Type) (P : foo X Y -> Prop),
             (forall x : X, P (bar X Y x)) ->
             (forall y : Y, P (baz X Y y)) ->
             (forall f1 : nat -> foo X Y,
               (forall n : nat, P (f1 n)) -> P (quux X Y f1)) ->
             forall f2 : foo X Y, P f2
*)
Inductive foo (X Y :Type) : Type :=
  | bar : X -> foo X Y
  | baz : Y -> foo X Y
  | quux : (nat -> foo X Y) -> foo X Y
.

Check foo_ind.

(** Exercise: 1 star, optional (foo')  *)
(** Consider the following inductive definition: *)

Inductive foo' (X:Type) : Type :=
  | C1 : list X -> foo' X -> foo' X
  | C2 : foo' X.

(** What induction principle will Coq generate for [foo']?  Fill
   in the blanks, then check your answer with Coq.)
     foo'_ind :
        forall (X : Type) (P : foo' X -> Prop),
              (forall (l : list X) (f : foo' X),
                    _______________________ ->
                    _______________________   ) ->
             ___________________________________________ ->
             forall f : foo' X, ________________________
*)

(** [] *)

(* ##################################################### *)
(** ** Induction Hypotheses *)

(** Where does the phrase "induction hypothesis" fit into this story?

    The induction principle for numbers
       forall P : nat -> Prop,
            P 0  ->
            (forall n : nat, P n -> P (S n))  ->
            forall n : nat, P n
   is a generic statement that holds for all propositions
   [P] (strictly speaking, for all families of propositions [P]
   indexed by a number [n]).  Each time we use this principle, we
   are choosing [P] to be a particular expression of type
   [nat->Prop].

   We can make the proof more explicit by giving this expression a
   name.  For example, instead of stating the theorem [mult_0_r] as
   "[forall n, n * 0 = 0]," we can write it as "[forall n, P_m0r
   n]", where [P_m0r] is defined as... *)

Definition P_m0r (n:nat) : Prop :=
  n * 0 = 0.

(** ... or equivalently... *)

Definition P_m0r' : nat->Prop :=
  fun n => n * 0 = 0.

(** Now when we do the proof it is easier to see where [P_m0r]
    appears. *)

Theorem mult_0_r'' : forall n:nat,
  P_m0r n.
Proof.
  apply nat_ind.
  - (* n = O *) reflexivity.
  - (* n = S n' *)
    (* Note the proof state at this point! *)
    intros n IHn.
    unfold P_m0r in IHn. unfold P_m0r. simpl. apply IHn. Qed.

(** This extra naming step isn't something that we'll do in
    normal proofs, but it is useful to do it explicitly for an example
    or two, because it allows us to see exactly what the induction
    hypothesis is.  If we prove [forall n, P_m0r n] by induction on
    [n] (using either [induction] or [apply nat_ind]), we see that the
    first subgoal requires us to prove [P_m0r 0] ("[P] holds for
    zero"), while the second subgoal requires us to prove [forall n',
    P_m0r n' -> P_m0r n' (S n')] (that is "[P] holds of [S n'] if it
    holds of [n']" or, more elegantly, "[P] is preserved by [S]").
    The _induction hypothesis_ is the premise of this latter
    implication -- the assumption that [P] holds of [n'], which we are
    allowed to use in proving that [P] holds for [S n']. *)

(* ##################################################### *)
(** ** More on the [induction] Tactic *)

(** The [induction] tactic actually does even more low-level
    bookkeeping for us than we discussed above.

    Recall the informal statement of the induction principle for
    natural numbers:
      - If [P n] is some proposition involving a natural number n, and
        we want to show that P holds for _all_ numbers n, we can
        reason like this:
          - show that [P O] holds
          - show that, if [P n'] holds, then so does [P (S n')]
          - conclude that [P n] holds for all n.
    So, when we begin a proof with [intros n] and then [induction n],
    we are first telling Coq to consider a _particular_ [n] (by
    introducing it into the context) and then telling it to prove
    something about _all_ numbers (by using induction).

    What Coq actually does in this situation, internally, is to
    "re-generalize" the variable we perform induction on.  For
    example, in our original proof that [plus] is associative...
*)

Theorem plus_assoc' : forall n m p : nat,
  n + (m + p) = (n + m) + p.
Proof.
  (* ...we first introduce all 3 variables into the context,
     which amounts to saying "Consider an arbitrary [n], [m], and
     [p]..." *)
  intros n m p.
  (* ...We now use the [induction] tactic to prove [P n] (that
     is, [n + (m + p) = (n + m) + p]) for _all_ [n],
     and hence also for the particular [n] that is in the context
     at the moment. *)
  induction n as [| n'].
  - (* n = O *) reflexivity.
  - (* n = S n' *)
    (* In the second subgoal generated by [induction] -- the
       "inductive step" -- we must prove that [P n'] implies
       [P (S n')] for all [n'].  The [induction] tactic
       automatically introduces [n'] and [P n'] into the context
       for us, leaving just [P (S n')] as the goal. *)
    simpl. rewrite -> IHn'. reflexivity.  Qed.

(** It also works to apply [induction] to a variable that is
   quantified in the goal. *)

Theorem plus_comm' : forall n m : nat,
  n + m = m + n.
Proof.
  induction n as [| n'].
  - (* n = O *) intros m. rewrite -> plus_0_r. reflexivity.
  - (* n = S n' *) intros m. simpl. rewrite -> IHn'.
    rewrite <- plus_n_Sm. reflexivity.  Qed.

(** Note that [induction n] leaves [m] still bound in the goal --
    i.e., what we are proving inductively is a statement beginning
    with [forall m].

    If we do [induction] on a variable that is quantified in the goal
    _after_ some other quantifiers, the [induction] tactic will
    automatically introduce the variables bound by these quantifiers
    into the context. *)

Theorem plus_comm'' : forall n m : nat,
  n + m = m + n.
Proof.
  (* Let's do induction on [m] this time, instead of [n]... *)
  induction m as [| m'].
  - (* m = O *) simpl. rewrite -> plus_0_r. reflexivity.
  - (* m = S m' *) simpl. rewrite <- IHm'.
    rewrite <- plus_n_Sm. reflexivity.  Qed.

(** **** Exercise: 1 star, optional (plus_explicit_prop)  *)
(** Rewrite both [plus_assoc'] and [plus_comm'] and their proofs in
    the same style as [mult_0_r''] above -- that is, for each theorem,
    give an explicit [Definition] of the proposition being proved by
    induction, and state the theorem and proof in terms of this
    defined proposition.  *)

(* FILL IN HERE *)
(** [] *)

(** ** Generalizing Inductions. *)

(** One potentially confusing feature of the [induction] tactic is
that it happily lets you try to set up an induction over a term
that isn't sufficiently general.  The net effect of this will be
to lose information (much as [destruct] can do), and leave
you unable to complete the proof. Here's an example: *)

Lemma one_not_beautiful_FAILED: ~ beautiful 1.
Proof.
  intro H.
  (* Just doing an [inversion] on [H] won't get us very far in the [b_sum]
    case. (Try it!). So we'll need induction. A naive first attempt: *)
  induction H.
  (* But now, although we get four cases, as we would expect from
     the definition of [beautiful], we lose all information about [H] ! *)
Abort.

(** The problem is that [induction] over a Prop only works properly over
   completely general instances of the Prop, i.e. one in which all
   the arguments are free (unconstrained) variables.
   In this respect it behaves more
   like [destruct] than like [inversion].

   When you're tempted to do use [induction] like this, it is generally
   an indication that you need to be proving something more general.
   But in some cases, it suffices to pull out any concrete arguments
   into separate equations, like this: *)

Lemma one_not_beautiful: forall n, n = 1 -> ~ beautiful n.
Proof.
 intros n E H.
  induction H  as [| | | p q Hp IHp Hq IHq].
    - (* b_0 *)
      inversion E.
    - (* b_3 *)
      inversion E.
    - (* b_5 *)
      inversion E.
    - (* b_sum *)
      (* the rest is a tedious case analysis *)
      destruct p as [|p'].
      + (* p = 0 *)
        destruct q as [|q'].
        * (* q = 0 *)
          inversion E.
        * (* q = S q' *)
          apply IHq. apply E.
      + (* p = S p' *)
        destruct q as [|q'].
        * (* q = 0 *)
          apply IHp.  rewrite plus_0_r in E. apply E.
        * (* q = S q' *)
          simpl in E. inversion E.  destruct p'.  inversion H0.  inversion H0.
Qed.

(** There's a handy [remember] tactic that can generate the second
proof state out of the original one. *)

Lemma one_not_beautiful': ~ beautiful 1.
Proof.
  intros H.
  remember 1 as n eqn:E.
  (* now carry on as above *)
  induction H.
Admitted.

(* ####################################################### *)
(** * Informal Proofs (Advanced) *)

(** Q: What is the relation between a formal proof of a proposition
       [P] and an informal proof of the same proposition [P]?

    A: The latter should _teach_ the reader how to produce the
       former.

    Q: How much detail is needed??

    Unfortunately, There is no single right answer; rather, there is a
    range of choices.

    At one end of the spectrum, we can essentially give the reader the
    whole formal proof (i.e., the informal proof amounts to just
    transcribing the formal one into words).  This gives the reader
    the _ability_ to reproduce the formal one for themselves, but it
    doesn't _teach_ them anything.

   At the other end of the spectrum, we can say "The theorem is true
   and you can figure out why for yourself if you think about it hard
   enough."  This is also not a good teaching strategy, because
   usually writing the proof requires some deep insights into the
   thing we're proving, and most readers will give up before they
   rediscover all the same insights as we did.

   In the middle is the golden mean -- a proof that includes all of
   the essential insights (saving the reader the hard part of work
   that we went through to find the proof in the first place) and
   clear high-level suggestions for the more routine parts to save the
   reader from spending too much time reconstructing these
   parts (e.g., what the IH says and what must be shown in each case
   of an inductive proof), but not so much detail that the main ideas
   are obscured.

   Another key point: if we're comparing a formal proof of a
   proposition [P] and an informal proof of [P], the proposition [P]
   doesn't change.  That is, formal and informal proofs are _talking
   about the same world_ and they _must play by the same rules_. *)
(** ** Informal Proofs by Induction *)

(** Since we've spent much of this chapter looking "under the hood" at
    formal proofs by induction, now is a good moment to talk a little
    about _informal_ proofs by induction.

    In the real world of mathematical communication, written proofs
    range from extremely longwinded and pedantic to extremely brief
    and telegraphic.  The ideal is somewhere in between, of course,
    but while you are getting used to the style it is better to start
    out at the pedantic end.  Also, during the learning phase, it is
    probably helpful to have a clear standard to compare against.
    With this in mind, we offer two templates below -- one for proofs
    by induction over _data_ (i.e., where the thing we're doing
    induction on lives in [Type]) and one for proofs by induction over
    _evidence_ (i.e., where the inductively defined thing lives in
    [Prop]).  In the rest of this course, please follow one of the two
    for _all_ of your inductive proofs. *)

(** *** Induction Over an Inductively Defined Set *)

(** _Template_:

       - _Theorem_: <Universally quantified proposition of the form
         "For all [n:S], [P(n)]," where [S] is some inductively defined
         set.>

         _Proof_: By induction on [n].

           <one case for each constructor [c] of [S]...>

           - Suppose [n = c a1 ... ak], where <...and here we state
             the IH for each of the [a]'s that has type [S], if any>.
             We must show <...and here we restate [P(c a1 ... ak)]>.

             <go on and prove [P(n)] to finish the case...>

           - <other cases similarly...>                        []

    _Example_:

      - _Theorem_: For all sets [X], lists [l : list X], and numbers
        [n], if [length l = n] then [index (S n) l = None].

        _Proof_: By induction on [l].

        - Suppose [l = []].  We must show, for all numbers [n],
          that, if [length [] = n], then [index (S n) [] =
          None].

          This follows immediately from the definition of index.

        - Suppose [l = x :: l'] for some [x] and [l'], where
          [length l' = n'] implies [index (S n') l' = None], for
          any number [n'].  We must show, for all [n], that, if
          [length (x::l') = n] then [index (S n) (x::l') =
          None].

          Let [n] be a number with [length l = n].  Since
            length l = length (x::l') = S (length l'),
          it suffices to show that
            index (S (length l')) l' = None.
]]
          But this follows directly from the induction hypothesis,
          picking [n'] to be [length l'].  [] *)

(** *** Induction Over an Inductively Defined Proposition *)

(** Since inductively defined proof objects are often called
    "derivation trees," this form of proof is also known as _induction
    on derivations_.

    _Template_:

       - _Theorem_: <Proposition of the form "[Q -> P]," where [Q] is
         some inductively defined proposition (more generally,
         "For all [x] [y] [z], [Q x y z -> P x y z]")>

         _Proof_: By induction on a derivation of [Q].  <Or, more
         generally, "Suppose we are given [x], [y], and [z].  We
         show that [Q x y z] implies [P x y z], by induction on a
         derivation of [Q x y z]"...>

           <one case for each constructor [c] of [Q]...>

           - Suppose the final rule used to show [Q] is [c].  Then
             <...and here we state the types of all of the [a]'s
             together with any equalities that follow from the
             definition of the constructor and the IH for each of
             the [a]'s that has type [Q], if there are any>.  We must
             show <...and here we restate [P]>.

             <go on and prove [P] to finish the case...>

           - <other cases similarly...>                        []

    _Example_

       - _Theorem_: The [<=] relation is transitive -- i.e., for all
         numbers [n], [m], and [o], if [n <= m] and [m <= o], then
         [n <= o].

         _Proof_: By induction on a derivation of [m <= o].

           - Suppose the final rule used to show [m <= o] is
             [le_n]. Then [m = o] and we must show that [n <= m],
             which is immediate by hypothesis.

           - Suppose the final rule used to show [m <= o] is
             [le_S].  Then [o = S o'] for some [o'] with [m <= o'].
             We must show that [n <= S o'].
             By induction hypothesis, [n <= o'].

             But then, by [le_S], [n <= S o'].  [] *)

(* ##################################################### *)
(** * Induction Principles in [Prop] (Advanced) *)

(** The remainder of this chapter offers some additional details on
    how induction works in Coq, the process of building proof trees,
    and the "trusted computing base" that underlies Coq proofs.  It
    can safely be skimmed on a first reading.  (As with the other
    advanced sections, we recommend skimming rather than skipping over
    it outright: it answers some questions that occur to many Coq
    users at some point, so it is useful to have a rough idea of
    what's here.) *)

(** Earlier, we looked in detail at the induction principles that Coq
    generates for inductively defined _sets_.  The induction
    principles for inductively defined _propositions_ like [gorgeous]
    are a tiny bit more complicated.  As with all induction
    principles, we want to use the induction principle on [gorgeous]
    to prove things by inductively considering the possible shapes
    that something in [gorgeous] can have -- either it is evidence
    that [0] is gorgeous, or it is evidence that, for some [n], [3+n]
    is gorgeous, or it is evidence that, for some [n], [5+n] is
    gorgeous and it includes evidence that [n] itself is.  Intuitively
    speaking, however, what we want to prove are not statements about
    _evidence_ but statements about _numbers_.  So we want an
    induction principle that lets us prove properties of numbers by
    induction on evidence.

    For example, from what we've said so far, you might expect the
    inductive definition of [gorgeous]...
    Inductive gorgeous : nat -> Prop :=
         g_0 : gorgeous 0
       | g_plus3 : forall n, gorgeous n -> gorgeous (3+m)
       | g_plus5 : forall n, gorgeous n -> gorgeous (5+m).
    ...to give rise to an induction principle that looks like this...
    gorgeous_ind_max :
       forall P : (forall n : nat, gorgeous n -> Prop),
            P O g_0 ->
            (forall (m : nat) (e : gorgeous m),
               P m e -> P (3+m) (g_plus3 m e)) ->
            (forall (m : nat) (e : gorgeous m),
               P m e -> P (5+m) (g_plus5 m e)) ->
            forall (n : nat) (e : gorgeous n), P n e
    ... because:

     - Since [gorgeous] is indexed by a number [n] (every [gorgeous]
       object [e] is a piece of evidence that some particular number
       [n] is gorgeous), the proposition [P] is parameterized by both
       [n] and [e] -- that is, the induction principle can be used to
       prove assertions involving both a gorgeous number and the
       evidence that it is gorgeous.

     - Since there are three ways of giving evidence of gorgeousness
       ([gorgeous] has three constructors), applying the induction
       principle generates three subgoals:

         - We must prove that [P] holds for [O] and [b_0].

         - We must prove that, whenever [n] is a gorgeous
           number and [e] is an evidence of its gorgeousness,
           if [P] holds of [n] and [e],
           then it also holds of [3+n] and [g_plus3 n e].

         - We must prove that, whenever [n] is a gorgeous
           number and [e] is an evidence of its gorgeousness,
           if [P] holds of [n] and [e],
           then it also holds of [5+n] and [g_plus5 n e].

     - If these subgoals can be proved, then the induction principle
       tells us that [P] is true for _all_ gorgeous numbers [n] and
       evidence [e] of their gorgeousness.

    But this is a little more flexibility than we actually need or
    want: it is giving us a way to prove logical assertions where the
    assertion involves properties of some piece of _evidence_ of
    gorgeousness, while all we really care about is proving
    properties of _numbers_ that are gorgeous -- we are interested in
    assertions about numbers, not about evidence.  It would therefore
    be more convenient to have an induction principle for proving
    propositions [P] that are parameterized just by [n] and whose
    conclusion establishes [P] for all gorgeous numbers [n]:
       forall P : nat -> Prop,
          ... ->
             forall n : nat, gorgeous n -> P n
    For this reason, Coq actually generates the following simplified
    induction principle for [gorgeous]: *)

Check gorgeous_ind.
(* ===>  gorgeous_ind
     : forall P : nat -> Prop,
       P 0 ->
       (forall n : nat, gorgeous n -> P n -> P (3 + n)) ->
       (forall n : nat, gorgeous n -> P n -> P (5 + n)) ->
       forall n : nat, gorgeous n -> P n *)

(** In particular, Coq has dropped the evidence term [e] as a
    parameter of the the proposition [P], and consequently has
    rewritten the assumption [forall (n : nat) (e: gorgeous n), ...]
    to be [forall (n : nat), gorgeous n -> ...]; i.e., we no longer
    require explicit evidence of the provability of [gorgeous n]. *)

(** In English, [gorgeous_ind] says:

    - Suppose, [P] is a property of natural numbers (that is, [P n] is
      a [Prop] for every [n]).  To show that [P n] holds whenever [n]
      is gorgeous, it suffices to show:

      - [P] holds for [0],

      - for any [n], if [n] is gorgeous and [P] holds for
        [n], then [P] holds for [3+n],

      - for any [n], if [n] is gorgeous and [P] holds for
        [n], then [P] holds for [5+n]. *)

(** As expected, we can apply [gorgeous_ind] directly instead of using [induction]. *)

Theorem gorgeous__beautiful' : forall n, gorgeous n -> beautiful n.
Proof.
   intros.
   apply gorgeous_ind.
   - (* g_0 *)
       apply b_0.
   - (* g_plus3 *)
       intros.
       apply b_sum. apply b_3.
       apply H1.
   - (* g_plus5 *)
       intros.
       apply b_sum. apply b_5.
       apply H1.
   - apply H.
Qed.

(** The precise form of an Inductive definition can affect the
    induction principle Coq generates.

For example, in [Logic], we have defined [<=] as: *)

(* Inductive le : nat -> nat -> Prop :=
     | le_n : forall n, le n n
     | le_S : forall n m, (le n m) -> (le n (S m)). *)

(** This definition can be streamlined a little by observing that the
    left-hand argument [n] is the same everywhere in the definition,
    so we can actually make it a "general parameter" to the whole
    definition, rather than an argument to each constructor. *)

Inductive le (n:nat) : nat -> Prop :=
  | le_n : le n n
  | le_S : forall m, (le n m) -> (le n (S m)).

Notation "m <= n" := (le m n).

(** The second one is better, even though it looks less symmetric.
    Why?  Because it gives us a simpler induction principle. *)

Check le_ind.
(* ===>  forall (n : nat) (P : nat -> Prop),
           P n ->
           (forall m : nat, n <= m -> P m -> P (S m)) ->
           forall n0 : nat, n <= n0 -> P n0 *)

(** By contrast, the induction principle that Coq calculates for the
    first definition has a lot of extra quantifiers, which makes it
    messier to work with when proving things by induction.  Here is
    the induction principle for the first [le]: *)

(* le_ind :
     forall P : nat -> nat -> Prop,
     (forall n : nat, P n n) ->
     (forall n m : nat, le n m -> P n m -> P n (S m)) ->
     forall n n0 : nat, le n n0 -> P n n0 *)

(* ##################################################### *)
(** * Additional Exercises *)

(** **** Exercise: 2 stars, optional (foo_ind_principle)  *)
(** Suppose we make the following inductive definition:
   Inductive foo (X : Set) (Y : Set) : Set :=
     | foo1 : X -> foo X Y
     | foo2 : Y -> foo X Y
     | foo3 : foo X Y -> foo X Y.
   Fill in the blanks to complete the induction principle that will be
   generated by Coq.
   foo_ind
        : forall (X Y : Set) (P : foo X Y -> Prop),
          (forall x : X, __________________________________) ->
          (forall y : Y, __________________________________) ->
          (________________________________________________) ->
           ________________________________________________

*)

(** [] *)

(** **** Exercise: 2 stars, optional (bar_ind_principle)  *)
(** Consider the following induction principle:
   bar_ind
        : forall P : bar -> Prop,
          (forall n : nat, P (bar1 n)) ->
          (forall b : bar, P b -> P (bar2 b)) ->
          (forall (b : bool) (b0 : bar), P b0 -> P (bar3 b b0)) ->
          forall b : bar, P b
   Write out the corresponding inductive set definition.
   Inductive bar : Set :=
     | bar1 : ________________________________________
     | bar2 : ________________________________________
     | bar3 : ________________________________________.

*)
(** [] *)

(** **** Exercise: 2 stars, optional (no_longer_than_ind)  *)
(** Given the following inductively defined proposition:
  Inductive no_longer_than (X : Set) : (list X) -> nat -> Prop :=
    | nlt_nil  : forall n, no_longer_than X [] n
    | nlt_cons : forall x l n, no_longer_than X l n ->
                               no_longer_than X (x::l) (S n)
    | nlt_succ : forall l n, no_longer_than X l n ->
                             no_longer_than X l (S n).
  write the induction principle generated by Coq.
  no_longer_than_ind
       : forall (X : Set) (P : list X -> nat -> Prop),
         (forall n : nat, ____________________) ->
         (forall (x : X) (l : list X) (n : nat),
          no_longer_than X l n -> ____________________ ->
                                  _____________________________ ->
         (forall (l : list X) (n : nat),
          no_longer_than X l n -> ____________________ ->
                                  _____________________________ ->
         forall (l : list X) (n : nat), no_longer_than X l n ->
           ____________________

*)
(** [] *)

(* ##################################################### *)
(** ** Induction Principles for other Logical Propositions *)

(** Similarly, in [Logic] we have defined [eq] as: *)

(* Inductive eq (X:Type) : X -> X -> Prop :=
       refl_equal : forall x, eq X x x. *)

(** In the Coq standard library, the definition of equality is
    slightly different: *)

Inductive eq' (X:Type) (x:X) : X -> Prop :=
    refl_equal' : eq' X x x.

(** The induction principle that Coq derives from this definition
    is the following: *)

Check eq'_ind.
(* ===>
     forall (X : Type) (x : X) (P : X -> Prop),
       P x -> forall y : X, x =' y -> P y *)

(*  ===>  (i.e., after a little reorganization)
     forall (X : Type) (x : X) forall y : X,
       x =' y ->
       forall P : X -> Prop, P x -> P y *)

(** This principle says that if [x] and [y] are equal then every
    property that is true of [x] is also true of [y], i.e. there is no
    context that distinguishes [x] and [y].  (Formally, this is the
    dual of a principle enunciated by Leibniz, which says that [x] and
    [y] are equal if they cannot be distinguished by any context. Note
    that the implication in this converse direction is trivially true
    in Coq: we simply instantiate [P] with the property of being equal
    to [x].  Leibniz took this principle itself as the _definition_ of
    equality, whereas in Coq it is a _consequence_ of defining
    equality as an inductive type.) *)

(** The induction principles for conjunction and disjunction are a
    good illustration of Coq's way of generating simplified induction
    principles for [Inductive]ly defined propositions, which we
    discussed above.  You try first: *)

(** **** Exercise: 1 star, optional (and_ind_principle)  *)
(** See if you can predict the induction principle for conjunction. *)

(* Check and_ind. *)
(** [] *)

(** **** Exercise: 1 star, optional (or_ind_principle)  *)
(** See if you can predict the induction principle for disjunction. *)

(* Check or_ind. *)
(** [] *)

Check and_ind.

(** From the inductive definition of the proposition [and P Q]
     Inductive and (P Q : Prop) : Prop :=
       conj : P -> Q -> (and P Q).
    we might expect Coq to generate this induction principle
     and_ind_max :
       forall (P Q : Prop) (P0 : P /\ Q -> Prop),
            (forall (a : P) (b : Q), P0 (conj P Q a b)) ->
            forall a : P /\ Q, P0 a
    but actually it generates this simpler and more useful one:
     and_ind :
       forall P Q P0 : Prop,
            (P -> Q -> P0) ->
            P /\ Q -> P0
    In the same way, when given the inductive definition of [or P Q]
     Inductive or (P Q : Prop) : Prop :=
       | or_introl : P -> or P Q
       | or_intror : Q -> or P Q.
    instead of the "maximal induction principle"
     or_ind_max :
       forall (P Q : Prop) (P0 : P \/ Q -> Prop),
            (forall a : P, P0 (or_introl P Q a)) ->
            (forall b : Q, P0 (or_intror P Q b)) ->
            forall o : P \/ Q, P0 o
    what Coq actually generates is this:
     or_ind :
       forall P Q P0 : Prop,
            (P -> P0) ->
            (Q -> P0) ->
            P \/ Q -> P0
]]
*)

(** **** Exercise: 1 star, optional (False_ind_principle)  *)
(** Can you predict the induction principle for falsehood? *)

(* Check False_ind. *)
(** [] *)

(** Here's the induction principle that Coq generates for existentials: *)

Check ex_ind.
(* ===>  forall (X:Type) (P: X->Prop) (Q: Prop),
         (forall witness:X, P witness -> Q) ->
          ex X P ->
           Q *)

(** This induction principle can be understood as follows: If we have
         a function [f] that can construct evidence for [Q] given _any_
        witness of type [X] together with evidence that this witness has
        property [P], then from a proof of [ex X P] we can extract the
        witness and evidence that must have been supplied to the
        constructor, give these to [f], and thus obtain a proof of [Q]. *)

(* ######################################################### *)
(** ** Explicit Proof Objects for Induction *)

(** Although tactic-based proofs are normally much easier to
    work with, the ability to write a proof term directly is sometimes
    very handy, particularly when we want Coq to do something slightly
    non-standard.  *)

(** Recall the induction principle on naturals that Coq generates for
    us automatically from the Inductive declation for [nat]. *)

Check nat_ind.
(* ===>
   nat_ind : forall P : nat -> Prop,
      P 0 ->
      (forall n : nat, P n -> P (S n)) ->
      forall n : nat, P n  *)

(** There's nothing magic about this induction lemma: it's just
   another Coq lemma that requires a proof.  Coq generates the proof
   automatically too...  *)

Print nat_ind.
Print nat_rect.
(* ===> (after some manual inlining and tidying)
   nat_ind =
    fun (P : nat -> Prop)
        (f : P 0)
        (f0 : forall n : nat, P n -> P (S n)) =>
          fix F (n : nat) : P n :=
             match n with
            | 0 => f
            | S n0 => f0 n0 (F n0)
            end.
*)

(** We can read this as follows:
     Suppose we have evidence [f] that [P] holds on 0,  and
     evidence [f0] that [forall n:nat, P n -> P (S n)].
     Then we can prove that [P] holds of an arbitrary nat [n] via
     a recursive function [F] (here defined using the expression
     form [Fix] rather than by a top-level [Fixpoint]
     declaration).  [F] pattern matches on [n]:
      - If it finds 0, [F] uses [f] to show that [P n] holds.
      - If it finds [S n0], [F] applies itself recursively on [n0]
         to obtain evidence that [P n0] holds; then it applies [f0]
         on that evidence to show that [P (S n)] holds.
    [F] is just an ordinary recursive function that happens to
    operate on evidence in [Prop] rather than on terms in [Set].

*)

(** We can adapt this approach to proving [nat_ind] to help prove
    _non-standard_ induction principles too.  Recall our desire to
    prove that

    [forall n : nat, even n -> ev n].

    Attempts to do this by standard induction on [n] fail, because the
    induction principle only lets us proceed when we can prove that
    [even n -> even (S n)] -- which is of course never provable.  What
    we did in [Logic] was a bit of a hack:

    [Theorem even__ev : forall n : nat,
     (even n -> ev n) /\ (even (S n) -> ev (S n))].

    We can make a much better proof by defining and proving a
    non-standard induction principle that goes "by twos": *)

Definition nat_ind2 :
   forall (P : nat -> Prop),
   P 0 ->
   P 1 ->
   (forall n : nat, P n -> P (S(S n))) ->
   forall n : nat , P n :=
      fun P => fun P0 => fun P1 => fun PSS =>
         fix f (n:nat) := match n with
                            0 => P0
                          | 1 => P1
                          | S (S n') => PSS n' (f n')
                         end.

(** Once you get the hang of it, it is entirely straightforward to
    give an explicit proof term for induction principles like this.
    Proving this as a lemma using tactics is much less intuitive (try
    it!).

    The [induction ... using] tactic variant gives a convenient way to
    specify a non-standard induction principle like this. *)

Lemma even__ev' : forall n, even n -> ev n.
Proof.
 intros.
 induction n as [ | |n'] using nat_ind2.
  - (* even 0 *)
    apply ev_0.
  - (* even 1 *)
    inversion H.
  - (* even (S(S n')) *)
    apply ev_SS.
    apply IHn'.  unfold even.  unfold even in H.  simpl in H. apply H.
Qed.

(* ######################################################### *)
(** ** The Coq Trusted Computing Base *)

(** One issue that arises with any automated proof assistant is "why
    trust it?": what if there is a bug in the implementation that
    renders all its reasoning suspect?

    While it is impossible to allay such concerns completely, the fact
    that Coq is based on the Curry-Howard correspondence gives it a
    strong foundation. Because propositions are just types and proofs
    are just terms, checking that an alleged proof of a proposition is
    valid just amounts to _type-checking_ the term.  Type checkers are
    relatively small and straightforward programs, so the "trusted
    computing base" for Coq -- the part of the code that we have to
    believe is operating correctly -- is small too.

    What must a typechecker do?  Its primary job is to make sure that
    in each function application the expected and actual argument
    types match, that the arms of a [match] expression are constructor
    patterns belonging to the inductive type being matched over and
    all arms of the [match] return the same type, and so on.

    There are a few additional wrinkles:

    - Since Coq types can themselves be expressions, the checker must
      normalize these (by using the computation rules) before
      comparing them.

    - The checker must make sure that [match] expressions are
      _exhaustive_.  That is, there must be an arm for every possible
      constructor.  To see why, consider the following alleged proof
      object:
      Definition or_bogus : forall P Q, P \/ Q -> P :=
        fun (P Q : Prop) (A : P \/ Q) =>
           match A with
           | or_introl H => H
           end.
      All the types here match correctly, but the [match] only
      considers one of the possible constructors for [or].  Coq's
      exhaustiveness check will reject this definition.

    - The checker must make sure that each [fix] expression
      terminates.  It does this using a syntactic check to make sure
      that each recursive call is on a subexpression of the original
      argument.  To see why this is essential, consider this alleged
      proof:
          Definition nat_false : forall (n:nat), False :=
             fix f (n:nat) : False := f n.
      Again, this is perfectly well-typed, but (fortunately) Coq will
      reject it. *)

(** Note that the soundness of Coq depends only on the correctness of
    this typechecking engine, not on the tactic machinery.  If there
    is a bug in a tactic implementation (and this certainly does
    happen!), that tactic might construct an invalid proof term.  But
    when you type [Qed], Coq checks the term for validity from
    scratch.  Only lemmas whose proofs pass the type-checker can be
    used in further proof developments.  *)

(** $Date: 2015-08-11 18:03:04 +0200 (Tue, 11 Aug 2015) $ *)

repo: Software-Foundations


text:
Require Import MirrorCore.TypesI.

Section SemiEqDecTyp.
  Context (typ : Type) {RType_typ : RType typ}.

  Class SemiEqDecTyp := {
    semi_eq_dec_typ : forall t (a b : typD t), option bool
  }.

  Class SemiEqDecTypOk (SemEq : SemiEqDecTyp) := {
    semi_eq_dec_typOk :
      forall t a b,
        match semi_eq_dec_typ t a b with
          | Some true => a = b
          | Some false => a <> b
          | None => True
        end
  }.

End SemiEqDecTyp.

Implicit Arguments SemiEqDecTypOk [[typ] [RType_typ]].
Implicit Arguments semi_eq_dec_typ [[typ] [RType_typ] [t] [SemiEqDecTyp]].
Implicit Arguments semi_eq_dec_typOk [[typ] [RType_typ] [SemEq] [SemiEqDecTypOk]].

Section SemiEqDecTypFacts.
  Context `{SemEqOk : SemiEqDecTypOk}.

  Lemma semi_eq_dec_typ_eq t (a b : typD t) (H : semi_eq_dec_typ a b = Some true) : a = b.
  Proof.
    destruct SemEqOk. specialize (semi_eq_dec_typOk0 t a b).
    rewrite H in semi_eq_dec_typOk0. apply semi_eq_dec_typOk0.
  Qed.

  Lemma semi_eq_dec_typ_neq t (a b : typD t) (H : semi_eq_dec_typ a b = Some false) : a <> b.
  Proof.
    destruct SemEqOk. specialize (semi_eq_dec_typOk0 t a b).
    rewrite H in semi_eq_dec_typOk0. apply semi_eq_dec_typOk0.
  Qed.

  Lemma semi_eq_dec_typ_refl t (a : typD t) b (H : semi_eq_dec_typ a a = Some b) : b = true.
  Proof.
    destruct SemEqOk. specialize (semi_eq_dec_typOk0 t a a).
    remember (semi_eq_dec_typ a a).
    destruct o; [destruct b0|]; inversion H.
    + reflexivity.
    + contradiction semi_eq_dec_typOk0. reflexivity.
  Qed.

End SemiEqDecTypFacts.

author: jesper-bengtson

repo: Charge

save_path: github-repos/coq/jesper-bengtson-Charge


text:
(*|
################################################
Proving that s-expressions printing is injective
################################################

:Link: https://stackoverflow.com/q/69617959
|*)

(*|
Question
********

I defined a type of s-expressions and it's printing functions.

.. coq:: none
|*)

Require Import Lists.List Strings.String.
Import ListNotations.

(*||*)

Inductive sexp : Set :=
  K : string -> list sexp -> sexp.

Fixpoint sexpprint (s : sexp) : list string :=
  match s with
    K n l => ["("%string]++[n]++(List.concat (map sexpprint l))++[")"%string]
  end.

(*|
(Yes, I understand it can be just string, not the list of strings, but
Coq have small amount of theorems for working with strings, but a big
amount for working with lists.)
|*)

(* more usual function *)
Fixpoint sexpprint' (s:sexp) :string :=
  match s with
    K n l => "(" ++ n ++ (String.concat "" (map sexpprint' l)) ++ ")"
  end.

(*|
And I've got stuck trying to prove this theorem:
|*)

Theorem sexpprint_inj s1 s2 :
  sexpprint s1 = sexpprint s2 -> s1 = s2.

(*|
Maybe there are some sources which can help me to plan the theorem's
proof? (books/articles/codes) How to prove it? (Maybe I need a special
kind of inductive principle, could you formulate its statement?)
|*)

(*|
Answer
******

The type ``sexp`` is an example of a *nested inductive type*, where
one of the recursive occurrences appears inside of another induction.
Such types are hard to work with in Coq, because the induction
principles that it generates by default are not useful. However, you
can fix this issue by writing down your own induction principle by
hand. Here is one possibility:

.. coq:: none
|*)

Reset Initial.
Require Import Coq.Lists.List Coq.Strings.String.
Import ListNotations.

(*||*)

Unset Elimination Schemes.
Inductive sexp : Type :=
| K : string -> list sexp -> sexp.
Set Elimination Schemes.

Definition tuple (T : sexp -> Type) (es : list sexp) :=
  fold_right (fun e R => T e * R)%type unit es.

Definition sexp_rect
           (T : sexp -> Type)
           (H : forall s es, tuple T es -> T (K s es)) :
  forall e, T e :=
  fix outer (e : sexp) : T e :=
    match e with
    | K s es =>
      let fix inner (es : list sexp) : tuple T es :=
          match es return tuple T es with
          | [] => tt
          | e :: es => (outer e, inner es)
          end in
      H s es (inner es)
    end.

Definition sexp_ind (T : sexp -> Prop) := sexp_rect T.

(*|
With this induction principle, it is now possible to prove your lemma
(exercise!), but you will need to generalize its statement a bit.

For a deeper discussion about these nested inductives, you can have a
look at `CPDT
<http://adam.chlipala.net/cpdt/html/Cpdt.InductiveTypes.html>`__.
|*)

author: vonavi

repo: coq-examples

save_path: github-repos/coq/vonavi-coq-examples


text:
(* Contribution to the Coq Library   V6.3 (July 1999)                    *)
Require Import securite.

Lemma POinvprel8 :
 forall (l l0 : list C) (k k0 k1 k2 : K) (c c0 c1 c2 : C)
   (d d0 d1 d2 d3 d4 d5 d6 d7 d8 d9 d10 d11 d12 d13 d14 d15 d16 d17 d18 d19
    d20 : D),
 inv0
   (ABSI (MBNaKab d7 d8 d9 k0) (MANbKabCaCb d4 d5 d6 k c c0)
      (MABNaNbKeyK d d0 d1 d2 d3) l) ->
 inv1
   (ABSI (MBNaKab d7 d8 d9 k0) (MANbKabCaCb d4 d5 d6 k c c0)
      (MABNaNbKeyK d d0 d1 d2 d3) l) ->
 invP
   (ABSI (MBNaKab d7 d8 d9 k0) (MANbKabCaCb d4 d5 d6 k c c0)
      (MABNaNbKeyK d d0 d1 d2 d3) l) ->
 rel8
   (ABSI (MBNaKab d7 d8 d9 k0) (MANbKabCaCb d4 d5 d6 k c c0)
      (MABNaNbKeyK d d0 d1 d2 d3) l)
   (ABSI (MBNaKab d18 d19 d20 k2) (MANbKabCaCb d15 d16 d17 k1 c1 c2)
      (MABNaNbKeyK d10 d11 d12 d13 d14) l0) ->
 invP
   (ABSI (MBNaKab d18 d19 d20 k2) (MANbKabCaCb d15 d16 d17 k1 c1 c2)
      (MABNaNbKeyK d10 d11 d12 d13 d14) l0).

Proof.
do 32 intro.
unfold rel8 in |- *; intros Inv0 Inv1 InvP and1.
elim and1; intros t1 and2; elim and2; intros t2 and3; elim and3;
 intros t3 and4; elim and4; intros eq_l0 t4.
elim eq_l0; assumption.
Qed.

author: coq-contribs

repo: otway-rees


text:
(*
 * Copyright (c) Meta Platforms, Inc. and affiliates.
 *
 * This source code is licensed under the MIT license found in the
 * LICENSE file in the root directory of this source tree.
 *)
From iris Require Import fancy_updates.
From iris.proofmode Require Import base tactics classes.
From iris.base_logic.lib Require Import iprop own wsat.

Section Modality.

(* Iris semantic context *)
Context `{Θ: gFunctors}.

(* Helper to iterate laters *)
Lemma laterN_soundness n (P : iProp Θ) : (⊢ ▷^n P) → ⊢ P.
Proof.
  elim : n => [ | n hi] //= h.
  apply uPred.later_soundness in h.
  by apply hi.
Qed.

Lemma bupd_elim (P Q: iProp Θ) : (Q -∗ (|==> P)) → (|==> Q) -∗ (|==> P).
Proof.
  move => ->.
  iIntros "H".
  by iMod "H".
Qed.

Lemma bupd_plainly_later (P : iProp Θ) : (▷ |==> ■ P) ⊢ |==> ▷ ◇ P.
Proof.
  iIntros "H".
  iModIntro.
  iNext.
  rewrite bupd_plainly.
  by auto.
Qed.

Lemma bupd_plain_later (P: iProp Θ) `{!Plain P} : (▷ |==> P) ⊢ |==> ▷ ◇ P.
Proof.  by rewrite {1}(plain P) bupd_plainly_later. Qed.

Notation "|=▷^ n Q" := (Nat.iter n (λ P, |==> ▷ P) Q)%I
    (at level 99, n at level 9, Q at level 200,
    format "|=▷^ n  Q") : bi_scope.

Lemma updN_zero (Q : iProp Θ) : (|=▷^0 Q) ⊣⊢ Q.
Proof. done. Qed.

Lemma updN_S n (Q : iProp Θ) :
  (|=▷^(S n) Q) ⊣⊢ |==> ▷ |=▷^n Q.
Proof. done. Qed.

Lemma updN_mono n (P Q : iProp Θ) :
  (P -∗ Q) → (|=▷^n P) -∗ (|=▷^n Q).
Proof.
  elim: n => [//|n HI H /=].
  iApply bupd_mono.
  iApply bi.later_mono.
  by iApply HI.
Qed.

Lemma updN_mono_I n (P Q : iProp Θ) :
  (P -∗ Q) -∗ (|=▷^n P) -∗ (|=▷^n Q).
Proof.
  elim: n => [|n hi]; first done.
  iIntros "H".
  rewrite !updN_S.
  iIntros "HH".
  iMod "HH".
  iModIntro.
  iNext.
  by iApply (hi with "H").
Qed.

Lemma updN_intro n (P: iProp Θ) : P -∗ (|=▷^n P).
Proof.
  elim: n => [// | n hi /=].
  iIntros "p".
  iApply bupd_intro.
  apply bi.later_mono in hi.
  by iApply hi.
Qed.

Lemma updN_sep n (P R: iProp Θ) : ((|=▷^n P) ∗ (|=▷^n R)) -∗ |=▷^n (P ∗ R).
Proof.
  elim: n => [// | n hi /=].
  iIntros "[H0 H1]".
  iMod "H0".
  iMod "H1".
  iModIntro.
  iNext.
  iApply hi.
  by iSplitL "H0".
Qed.

Lemma updN_frame_r n (P R: iProp Θ) : (|=▷^n P) ∗ R -∗ |=▷^n P ∗ R.
Proof.
  elim: n => [// | n hi /=].
  iIntros "[H HR]".
  iMod "H"; iModIntro.
  iNext.
  iApply hi.
  by iSplitL "H".
Qed.

Lemma updN_plus n1 (P: iProp Θ) : ∀ n2,
  (|=▷^n1 P) -∗ (|=▷^(n1 + n2) P).
Proof.
  elim:n1 => [ | n1 hi] /= => n2; iIntros "h1"; first by iApply updN_intro.
  iMod "h1".
  iModIntro.
  iNext.
  by iApply hi.
Qed.

Lemma step_upd_plain (P: iProp Θ) `{!Plain P} : (|==> ▷ |==> P) -∗ |==> ▷ ◇ P.
Proof.
  apply bupd_elim.
  by rewrite bupd_plain_later.
Qed.

Lemma step_updN_plain n (P: iProp Θ) `{!Plain P} : (|=▷^n P) -∗ |==> ▷^n ◇ P.
Proof.
  elim : n => [ | n hi] /=.
  - rewrite -bupd_intro; by auto.
  - rewrite hi step_upd_plain.
    apply bupd_mono.
    by rewrite bi.except_0_laterN bi.except_0_idemp.
Qed.

End Modality.

Notation "|=▷^ n Q" := (Nat.iter n (λ P, |==> ▷ P) Q)%I
    (at level 99, n at level 9, Q at level 200,
    format "|=▷^ n  Q") : bi_scope.

Lemma step_updN_soundness Θ n φ: (⊢@{iPropI Θ} |==> |=▷^n ⌜ φ ⌝) → φ.
Proof.
  move => Hiter.
  eapply uPred.pure_soundness.
  apply (uPred.laterN_soundness _ (S n)); simpl.
  apply uPred.bupd_soundness.
  { rewrite -bi.later_laterN.
    apply laterN_plain.
    by apply pure_plain.
  }
  iPoseProof Hiter as "H". clear Hiter.
  iMod (step_updN_plain with "H") as "H2".
  iMod "H2".
  iModIntro.
  rewrite -bi.later_laterN bi.laterN_later.
  iNext. iMod "H2" as %Hφ. auto.
Qed.

Print Assumptions step_updN_soundness.

author: facebookresearch

repo: shack

save_path: github-repos/coq/facebookresearch-shack


text:
(* Copyright (c) 2019 by Swirlds, Inc.
   Implemented by Karl Crary.
*)

Require Import Nat.
Require Import List.
Require Import Decidable.
Require Import Omega.
Require Import Permutation.

Require Import Tact.
Require Import Decide.

Definition sumweight {T : Type} (f : T -> nat) (l : list T) : nat
  :=
  fold_right (fun x m => f x + m) 0 l.

Lemma sumweight_cons :
  forall (T : Type) (f : T -> nat) (x : T) (l : list T),
    sumweight f (cons x l) = f x + sumweight f l.
Proof.
intros T f x l.
reflexivity.
Qed.

Lemma sumweight_app :
  forall (T : Type) (f : T -> nat) (p q : list T),
    sumweight f (p ++ q) = sumweight f p + sumweight f q.
Proof.
intros T f p q.
induct p; eauto.

(* cons *)
{
intros x l IH.
rewrite <- app_comm_cons.
rewrite -> !sumweight_cons.
omega.
}
Qed.

Lemma NoDup_app :
  forall (T : Type) (p q : list T),
    NoDup p
    -> NoDup q
    -> (forall x, In x p -> In x q -> False)
    -> NoDup (p ++ q).
Proof.
intros T p q Hdistp Hdistq Hdisj.
revert Hdistp Hdisj.
induct p.

(* nil *)
{
intros _ _.
exact Hdistq.
}

(* cons *)
{
intros x p IH Hdistxp Hdisj.
cbn.
invert Hdistxp.
intros Hnotin Hdistp.
apply NoDup_cons.
  {
  intro Hin.
  so (in_app_or _#4 Hin) as [Hinp | Hinq].
    { contradiction. }

    {
    eapply Hdisj; eauto.
    left; reflexivity.
    }
  }

  {
  apply IH; auto.
  intros y Hinp Hinq.
  eapply Hdisj; eauto.
  right; auto.
  }
}
Qed.

Lemma permutation_weight :
  forall (T : Type) (f : T -> nat) (p q : list T),
    Permutation p q
    -> sumweight f p = sumweight f q.
Proof.
intros T f p q Hperm.
induct Hperm; auto.

(* skip *)
{
intros x p q _ IH.
cbn.
f_equal; auto.
}

(* swap *)
{
intros x y p.
cbn.
omega.
}

(* trans *)
{
intros p q r _ IH1 _ IH2.
etransitivity; eauto.
}
Qed.

Lemma permutation_weight' :
  forall (T : Type) (f : T -> nat) (p q : list T),
    NoDup p
    -> NoDup q
    -> (forall x, In x p <-> In x q)
    -> sumweight f p = sumweight f q.
Proof.
intros T f p q Hdistp Hdistq Hiff.
apply permutation_weight.
apply NoDup_Permutation; auto.
Qed.

Lemma incl_weight :
  forall (T : Type) (f : T -> nat) (p q : list T),
    NoDup p
    -> NoDup q
    -> List.incl p q
    -> sumweight f p <= sumweight f q.
Proof.
intros T f p q Hp Hq Hpq.
revert q Hq Hpq.
induct Hp.

(* nil *)
{
intros q Hq Hpq.
cbn.
omega.
}

(* cons *)
{
intros x p Hnotin Hdistp IH q Hq Hpq.
rewrite -> sumweight_cons.
assert (In x q) as Hin.
  {
  apply Hpq.
  left; auto.
  }
so (in_split _#3 Hin) as (q1 & q2 & ->).
rewrite -> sumweight_app.
rewrite -> sumweight_cons.
exploit (IH (q1 ++ q2)) as H.
  {
  eapply NoDup_remove_1; eauto.
  }

  {
  intros y Hy.
  so (in_app_or _#4 (Hpq y (or_intror Hy))) as [Hiny | Hiny].
    {
    apply in_or_app; left; auto.
    }

    {
    destruct Hiny as [Heq | Hiny].
      {
      subst y.
      contradiction.
      }

      {
      apply in_or_app; right; auto.
      }
    }
  }
rewrite -> sumweight_app in H.
omega.
}
Qed.

Lemma inclusion_exclusion :
  forall T (f : T -> nat) (p q u : list T),
    (forall (x y : T), decidable (x = y))
    -> NoDup p
    -> NoDup q
    -> NoDup u
    -> List.incl p u
    -> List.incl q u
    -> exists r,
         NoDup r
         /\ List.incl r p
         /\ List.incl r q
         /\ sumweight f r >= sumweight f p + sumweight f q - sumweight f u.
Proof.
intros T f p q u Hdeceq Hp Hq Hu Hpu Hqu.
revert q u Hq Hu Hpu Hqu.
induct Hp.

(* nil *)
{
intros q u Hq Hu Hpu Hqu.
exists nil.
do2 3 split.
  {
  apply NoDup_nil.
  }

  {
  intros x Hx.
  destruct Hx.
  }

  {
  intros x Hx.
  destruct Hx.
  }
cbn.
so (incl_weight _ f _ _ Hq Hu Hqu).
omega.
}

(* cons *)
{
intros x p Hnotin Hp IH q u Hq Hu Hpu Hqu.
assert (In x u) as Hinu.
  {
  apply Hpu.
  left; reflexivity.
  }
so (in_split _#3 Hinu) as (u1 & u2 & ->).
assert (List.incl p (u1 ++ u2)) as Hpu'.
  {
  intros y Hyp.
  assert (In y (x :: p)) as Hyp'.
    {
    right; auto.
    }
  so (in_app_or _#4 (Hpu _ Hyp')) as [Hyu1 | Hyu2].
    {
    apply in_or_app; auto.
    }

    {
    apply in_or_app; right.
    cbn in Hyu2.
    destruct Hyu2; auto.
    exfalso.
    subst y.
    contradiction.
    }
  }
so (dec_In _ x q Hdeceq) as [Hinq | Hnin].
  {
  so (in_split _#3 Hinq) as (q1 & q2 & ->).
  exploit (IH (q1 ++ q2) (u1 ++ u2)) as H; eauto using NoDup_remove_1.
    {
    intros y Hyq.
    assert (In y (q1 ++ x :: q2)) as Hyq'.
      {
      so (in_app_or _#4 Hyq) as [Hyq1 | Hyq2].
        {
        apply in_or_app; auto.
        }

        {
        apply in_or_app; right.
        right.
        auto.
        }
      }
    so (Hqu y Hyq') as Hyu.
    so (in_app_or _#4 Hyu) as [Hyu1 | Hyu2].
      {
      apply in_or_app; auto.
      }

      {
      destruct Hyu2 as [Heq | Hyu2'].
        {
        exfalso.
        subst y.
        so (NoDup_remove_2 _#4 Hq).
        contradiction.
        }

        {
        apply in_or_app; auto.
        }
      }
    }
  destruct H as (r & Hr & Hrp & Hrq & Hlen).
  exists (x :: r).
  do2 3 split.
    {
    apply NoDup_cons; auto.
    }

    {
    intros y Hy.
    destruct Hy as [| Hy'].
      {
      subst y.
      left; auto.
      }

      {
      right.
      apply Hrp; auto.
      }
    }

    {
    intros y Hy.
    destruct Hy as [| Hy'].
      {
      subst y.
      apply in_or_app.
      right; left; auto.
      }

      {
      so (Hrq y Hy') as Hyq.
      so (in_app_or _#4 Hyq) as [Hyq' | Hyq'].
        {
        apply in_or_app; auto.
        }

        {
        apply in_or_app; right; right; auto.
        }
      }
    }

    {
    rewrite -> !sumweight_app, !sumweight_cons.
    rewrite -> !sumweight_app in Hlen.
    omega.
    }
  }

  {
  exploit (IH q (u1 ++ u2)) as H; eauto using NoDup_remove_1.
    {
    intros y Hy.
    so (Hqu y Hy) as Hyu.
    so (in_app_or _#4 Hyu) as [Hyu' | Hyu'].
      {
      apply in_or_app; auto.
      }

      {
      destruct Hyu' as [| Hyu''].
        {
        subst y.
        contradiction.
        }

        {
        apply in_or_app; auto.
        }
      }
    }
  destruct H as (r & Hr & Hrp & Hrq & Hlen).
  exists r.
  do2 3 split; auto.
    {
    intros y Hy.
    right; auto.
    }

    {
    rewrite -> !sumweight_app, !sumweight_cons.
    rewrite -> !sumweight_app in Hlen.
    omega.
    }
  }
}
Qed.

Lemma enumerate_subset :
  forall T (P : T -> Prop) (u : list T),
    (forall x, In x u -> decidable (P x))
    -> NoDup u
    -> exists p,
         NoDup p
         /\ forall x, In x p <-> (P x /\ In x u).
Proof.
intros T P u.
induct u.

(* nil *)
{
intros _ _.
exists nil.
split; auto using NoDup_nil.
intro x.
split.
  {
  intro H.
  destruct H.
  }

  {
  intros (_ & ?); auto.
  }
}

(* cons *)
{
intros x u IH Hdec Hdist.
invertc Hdist.
intros Hnotin Hdist.
exploit IH as H; auto.
  {
  intros y Hin.
  apply Hdec.
  right; auto.
  }
destruct H as (p & Hdistp & Hp).
so (Hdec x (or_introl (eq_refl _))) as [Hyes | Hno].
  {
  exists (cons x p).
  split.
    {
    apply NoDup_cons; auto.
    contradict Hnotin.
    apply Hp; auto.
    }
  intros y.
  split.
    {
    intro Hy.
    destruct Hy as [Heq | Hy].
      {
      subst y.
      split; auto.
      left; auto.
      }
    split.
      {
      apply Hp; auto.
      }

      {
      right.
      apply Hp; auto.
      }
    }

    {
    intros (Hy & Hiny).
    destruct Hiny as [Heq | Hiny].
      {
      subst y.
      left; auto.
      }

      {
      right.
      apply Hp; auto.
      }
    }
  }

  {
  exists p.
  split; auto.
  intro y.
  split.
    {
    intro Hy.
    split.
      {
      apply Hp; auto.
      }

      {
      right.
      apply Hp; auto.
      }
    }

    {
    intros (Hy & Hiny).
    destruct Hiny as [Heq | Hiny].
      {
      subst y.
      contradiction.
      }

      {
      apply Hp; auto.
      }
    }
  }
}
Qed.

Lemma deduplicate :
  forall T (l : list T),
    (forall (x y : T), decidable (x = y))
    -> exists l',
         NoDup l'
         /\ (forall x, In x l <-> In x l').
Proof.
intros T l Hdec.
induct l.

(* nil *)
{
exists nil.
split.
  { apply NoDup_nil. }
intros x; split; intro H; destruct H.
}

(* cons *)
{
intros x l IH.
destruct IH as (l' & Hdist & Hl').
so (dec_In _ x l' Hdec) as [Hin | Hnin].
  {
  exists l'.
  split; auto.
  intro y.
  split.
    {
    intro H.
    destruct H as [Heq | Hin'].
      {
      subst y; auto.
      }

      {
      apply Hl'; auto.
      }
    }

    {
    intro Hy.
    right.
    apply Hl'; auto.
    }
  }

  {
  exists (cons x l').
  split.
    {
    apply NoDup_cons; auto.
    }

    {
    intros y.
    split.
      {
      intro H.
      destruct H as [Heq | Hin'].
        {
        subst y; left; auto.
        }

        {
        right.
        apply Hl'; auto.
        }
      }

      {
      intro Hy.
      destruct Hy as [Heq | Hin].
        {
        subst; left; auto.
        }

        {
        right.
        apply Hl'; auto.
        }
      }
    }
  }
}
Qed.

Definition weight {T : Type} (f : T -> nat) (P : T -> Prop) (n : nat) : Prop
  :=
  exists l,
    NoDup l
    /\ (forall x, P x <-> In x l)
    /\ sumweight f l = n.

Lemma weight_empty :
  forall T f, weight f (fun (x : T) => False) 0.
Proof.
intros T f.
exists nil.
do2 2 split; auto.
  { apply NoDup_nil. }

  {
  intros x.
  cbn.
  split; auto.
  }
Qed.

Lemma weight_singleton :
  forall (T : Type) (f : T -> nat) (x : T),
    weight f (fun y => y = x) (f x).
Proof.
intros T f x.
exists (cons x nil).
do2 2 split; auto.
  {
  apply NoDup_cons.
    {
    intro H.
    destruct H.
    }

    { apply NoDup_nil. }
  }

  {
  intros y.
  split.
    {
    intros ->.
    left; auto.
    }

    {
    intro H.
    destruct H as [-> | H]; auto.
    destruct H.
    }
  }

  {
  cbn.
  omega.
  }
Qed.

Lemma weight_In :
  forall (T : Type) (f : T -> nat) (l : list T),
    NoDup l
    -> weight f (fun x => In x l) (sumweight f l).
Proof.
intros T f l.
exists l.
do2 2 split; auto.
intro; split; auto.
Qed.

Lemma weight_fun :
  forall (T : Type) (f : T -> nat) (P : T -> Prop) n n',
    weight f P n
    -> weight f P n'
    -> n = n'.
Proof.
intros T f P n n' Hn Hn'.
destruct Hn as (l & Hnodup & Hmem & <-).
destruct Hn' as (l' & Hnodup' & Hmem' & <-).
eapply permutation_weight'; eauto.
intro x.
split; intro Hx.
  {
  apply Hmem'; apply Hmem; auto.
  }

  {
  apply Hmem; apply Hmem'; auto.
  }
Qed.

Lemma weight_iff :
  forall (T : Type) (f : T -> nat) (P Q : T -> Prop) n,
    (forall x, P x <-> Q x)
    -> weight f P n
    -> weight f Q n.
Proof.
intros T f P Q n Hiff HP.
destruct HP as (p & Hdist & Hp & Hlen).
exists p.
do2 2 split; auto.
intros x.
split.
  {
  intro Hx.
  apply Hp.
  apply Hiff.
  auto.
  }

  {
  intro Hx.
  apply Hiff.
  apply Hp.
  auto.
  }
Qed.

Lemma weight_empty' :
  forall T (f : T -> nat) (P : T -> Prop),
    (forall x, ~ P x)
    -> weight f P 0.
Proof.
intros T f P Hfalse.
apply (weight_iff _ _ (fun _ => False)).
  2:{ apply weight_empty. }
intros x.
split.
 { intro H; destruct H. }

 { apply Hfalse. }
Qed.

Lemma weight_nonempty :
  forall T (f : T -> nat) (P : T -> Prop) p,
    weight f P p
    -> p > 0
    -> exists x, P x.
Proof.
intros T f P p Hp Hgt.
destruct Hp as (l & _ & Hl & Hlen).
destruct l as [| x l].
  {
  cbn in Hlen.
  omega.
  }

  {
  exists x.
  apply Hl.
  left; auto.
  }
Qed.

Lemma weight_subset :
  forall (T : Type) (f : T -> nat) (P Q : T -> Prop) n,
    (forall x, Q x -> decidable (P x))
    -> incl P Q
    -> weight f Q n
    -> exists m,
         weight f P m
         /\ m <= n.
Proof.
intros T f P Q n HdecP HPQ HcardQ.
destruct HcardQ as (q & Hdistq & Hq & Hlenq).
exploit (enumerate_subset _ P q) as H; auto.
  {
  intros x Hx.
  apply HdecP.
  apply Hq; auto.
  }
destruct H as (p & Hdistp & Hp).
exists (sumweight f p).
split.
  {
  exists p.
  do2 2 split; auto.
  intro x.
  split.
    {
    intro Hx.
    apply Hp.
    split; auto.
    apply Hq; auto.
    }

    {
    intro Hx.
    apply Hp; auto.
    }
  }

  {
  subst n.
  apply incl_weight; auto.
  intros x Hx.
  apply Hq.
  apply HPQ.
  apply Hp; auto.
  }
Qed.

Lemma weight_subset' :
  forall (T : Type) (f : T -> nat) (P Q : T -> Prop) m n,
    (forall x, Q x -> decidable (P x))
    -> incl P Q
    -> weight f P m
    -> weight f Q n
    -> m <= n.
Proof.
intros T f P Q m n Hdec Hincl HwtP HwtQ.
so (weight_subset _#5 Hdec Hincl HwtQ) as (m' & HwtP' & Hle).
so (weight_fun _#5 HwtP HwtP'); subst m'.
exact Hle.
Qed.

Lemma weight_sum :
  forall T (f : T -> nat) (A B : T -> Prop) a b,
    weight f A a
    -> weight f B b
    -> (forall x, A x -> B x -> False)
    -> weight f (fun x => A x \/ B x) (a + b).
Proof.
intros T f A B a b Ha Hb Hdisj.
destruct Ha as (l & Hdistl & Hl & Hlenl).
destruct Hb as (m & Hdistm & Hm & Hlenm).
subst a b.
exists (l ++ m).
do2 2 split.
  {
  apply NoDup_app; auto.
  intros x Hxl Hxm.
  apply (Hdisj x).
    { apply Hl; auto. }

    { apply Hm; auto. }
  }

  {
  intros x.
  split.
    {
    intros [Hx | Hx].
      {
      apply in_or_app; left.
      apply Hl; auto.
      }

      {
      apply in_or_app; right.
      apply Hm; auto.
      }
    }

    {
    intros Hx.
    so (in_app_or _#4 Hx) as [Hxl | Hxm].
      {
      left.
      apply Hl; auto.
      }

      {
      right.
      apply Hm; auto.
      }
    }
  }

  {
  rewrite -> sumweight_app.
  reflexivity.
  }
Qed.

Lemma NoDup_weight_incl :
  forall T (f : T -> nat) (l l' : list T),
    NoDup l
    -> (forall x, In x l' -> f x > 0)
    -> sumweight f l' <= sumweight f l
    -> List.incl l l'
    -> List.incl l' l.
Proof.
intros T f l m Hdist Hpos Hle Hlm.
remember (sumweight f m) as w eqn:Heqw.
revert l m Hdist Hpos Hle Hlm Heqw.
wfinduct w using lt_wf.
intros w IH l m Hdist Hpos Hle Hlm ->.
destruct l as [| x l].
  {
  destruct m as [| x m]; auto.
  rewrite -> sumweight_cons in Hle.
  cbn in Hle.
  so (Hpos x (or_introl (eq_refl _))).
  omega.
  }
so (Hlm x (or_introl (eq_refl _))) as Hmx.
so (in_split _#3 Hmx) as (m1 & m2 & ->).
cut (List.incl (m1 ++ m2) l).
  {
  intros Hincl y Hy.
  so (in_app_or _#4 Hy) as [Hy' | Hy'].
    {
    right.
    apply Hincl.
    apply in_or_app.
    left; auto.
    }

    {
    destruct Hy' as [| Hy'].
      {
      subst y.
      left; auto.
      }

      {
      right.
      apply Hincl.
      apply in_or_app; right; auto.
      }
    }
  }
invertc Hdist.
intros Hnotin Hdist.
apply (IH (sumweight f (m1 ++ m2))); auto.
  {
  rewrite -> !sumweight_app.
  rewrite -> sumweight_cons.
  exploit (Hpos x) as Hpos'.
    {
    apply in_or_app; right; left; auto.
    }
  omega.
  }

  {
  intros y Hy.
  apply Hpos.
  revert y Hy.
  apply incl_app.
    {
    apply incl_appl.
    apply incl_refl.
    }

    {
    apply incl_appr.
    apply incl_tl.
    apply incl_refl.
    }
  }

  {
  rewrite -> sumweight_app.
  rewrite -> sumweight_app in Hle.
  rewrite -> !sumweight_cons in Hle.
  omega.
  }

  {
  intros y Hy.
  so (in_app_or _#4 (Hlm y (or_intror Hy))) as [Hy' | Hy'].
    {
    apply in_or_app; left; auto.
    }

    {
    destruct Hy' as [| Hy'].
      {
      subst y.
      contradiction.
      }

      {
      apply in_or_app; right; auto.
      }
    }
  }
Qed.

Lemma weight_partition :
  forall T (f : T -> nat) (A B U : T -> Prop) a b,
    incl A U
    -> incl B U
    -> (forall x, U x -> f x > 0)
    -> weight f U (a + b)
    -> weight f A a
    -> weight f B b
    -> (forall x, A x -> B x -> False)
    -> forall x, U x -> A x \/ B x.
Proof.
intros T f A B U m n HAU HBU Hpos HcardU HcardA HcardB Hdisj.
destruct HcardU as (u & Hdistu & Hu & Hlenu).
destruct HcardA as (a & Hdista & Ha & Hlena).
destruct HcardB as (b & Hdistb & Hb & Hlenb).
assert (forall x, In x u -> In x (a ++ b)) as Hprop.
  {
  apply (NoDup_weight_incl _ f); auto.
    {
    apply NoDup_app; auto.
    intros x Hxa Hxb.
    apply (Hdisj x).
      { apply Ha; auto. }

      { apply Hb; auto. }
    }

    {
    intros x Hx.
    apply Hpos.
    apply Hu; auto.
    }

    {
    rewrite -> sumweight_app.
    omega.
    }

    {
    intros x Hx.
    so (in_app_or _#4 Hx) as [Hx' | Hx'].
      {
      apply Hu.
      apply HAU.
      apply Ha; auto.
      }

      {
      apply Hu.
      apply HBU.
      apply Hb; auto.
      }
    }
  }
intros x Hx.
so (in_app_or _#4 (Hprop x (Hu x andel Hx))) as [Hx' | Hx'].
  {
  left.
  apply Ha; auto.
  }

  {
  right.
  apply Hb; auto.
  }
Qed.

Lemma weight_difference :
  forall T (f : T -> nat) (A B : T -> Prop) a b,
    (forall (x y : T), decidable (x = y))
    -> weight f A a
    -> weight f B b
    -> a < b
    -> exists x, ~ A x /\ B x.
Proof.
intros T f A B m n Hdec HcardA HcardB Hlt.
destruct HcardA as (a & Hdista & Ha & Hlena).
destruct HcardB as (b & Hdistb & Hb & Hlenb).
cut (exists x, ~ In x a /\ In x b).
  {
  intros (x & Hnin & Hin).
  exists x.
  split.
    {
    contradict Hnin.
    apply Ha; auto.
    }

    {
    apply Hb; auto.
    }
  }
clear Ha Hb Hdista.
subst m n.
revert a Hlt.
induct Hdistb.

(* nil *)
{
intros a Hlen.
cbn in Hlen.
omega.
}

(* cons *)
{
intros x b Hninb Hdistb IH a Hlen.
so (dec_In _ x a Hdec) as [Hin | Hnina].
  {
  so (in_split _#3 Hin) as (a1 & a2 & ->).
  exploit (IH (a1 ++ a2)) as H.
    {
    rewrite -> sumweight_app in Hlen |- *.
    rewrite -> !sumweight_cons in Hlen.
    omega.
    }
  destruct H as (y & Hnina & Hinb).
  exists y.
  split.
    {
    contradict Hnina.
    so (in_app_or _#4 Hnina) as [Hina | Hina].
      { apply in_or_app; left; auto. }
    destruct Hina as [Heq | Hina].
      {
      subst y.
      contradiction.
      }
    apply in_or_app; right; auto.
    }

    {
    right; auto.
    }
  }

  {
  exists x.
  split; auto.
  left; auto.
  }
}
Qed.

Lemma weight_corr_le :
  forall S T (f : S -> nat) (g : T -> nat) (P : S -> Prop) (Q : T -> Prop) (R : S -> T -> Prop) p q,
    (forall x x' y, P x -> P x' -> Q y -> R x y -> R x' y -> x = x')
    -> (forall x, P x -> exists y, R x y /\ Q y /\ f x <= g y)
    -> weight f P p
    -> weight g Q q
    -> p <= q.
Proof.
intros S T f g P Q R np nq Hinj Hdef HcardP HcardQ.
destruct HcardP as (p & Hdistp & Hp & Hlenp).
destruct HcardQ as (q & Hdistq & Hq & Hlenq).
subst np nq.
cut (exists r,
       NoDup r
       /\ (forall x, In x r -> Q x /\ exists y, In y p /\ R y x)
       /\ sumweight f p <= sumweight g r).
  {
  intros (r & Hdistr & Hr & Hlenr).
  rewrite -> Hlenr.
  apply incl_weight; auto.
  intros x Hx.
  apply Hq.
  apply Hr; auto.
  }
so (fun x => Hp x ander) as H.
clear Hp.
revert H.
induct Hdistp.

(* nil *)
{
intros _.
exists nil.
do2 2 split; auto.
  { apply NoDup_nil. }
intros x Hx.
destruct Hx.
}

(* cons *)
{
intros x p Hnin _ IH Hp.
exploit (Hp x) as Hx.
  {
  left; auto.
  }
so (Hdef x Hx) as (y & Hxy & Hy & Hle).
exploit IH as H.
  {
  intros z Hz.
  apply Hp.
  right; auto.
  }
destruct H as (r & Hdistr & Hr & Hlenr).
exists (cons y r).
do2 2 split.
  {
  apply NoDup_cons; auto.
  contradict Hnin.
  so (Hr y Hnin) as (_ & x' & Hinx' & Hx'y).
  so (Hinj x x' y Hx (Hp x' (or_intror Hinx')) Hy Hxy Hx'y).
  subst x'.
  exact Hinx'.
  }

  {
  intros z Hz.
  destruct Hz as [Heq | Hz].
    {
    subst z.
    split; auto.
    exists x.
    split; auto.
    left; auto.
    }

    {
    so (Hr z Hz) as (HQz & w & Hinw & Hwz).
    split; auto.
    exists w.
    split; auto.
    right; auto.
   }
  }

  {
  rewrite -> !sumweight_cons.
  omega.
  }
}
Qed.

Lemma weight_corr_eq :
  forall S T (f : S -> nat) (g : T -> nat) (P : S -> Prop) (Q : T -> Prop) (R : S -> T -> Prop) p q,
    (forall x x' y, P x -> P x' -> Q y -> R x y -> R x' y -> x = x')
    -> (forall x y y', P x -> Q y -> Q y' -> R x y -> R x y' -> y = y')
    -> (forall x, P x -> exists y, R x y /\ Q y /\ f x = g y)
    -> (forall y, Q y -> exists x, R x y /\ P x /\ f x = g y)
    -> weight f P p
    -> weight g Q q
    -> p = q.
Proof.
intros S T f g P Q R p q Hinj Hfun Hdef Hsur HcardP HcardQ.
exploit (weight_corr_le S T f g P Q R p q); auto.
  {
  intros x Hx.
  so (Hdef x Hx) as (y & Hxy & Hy & Heq).
  exists y.
  do2 2 split; auto.
  omega.
  }
exploit (weight_corr_le T S g f Q P (fun x y => R y x) q p); auto.
  {
  intros.
  eapply Hfun; eauto.
  }

  {
  intros x Hx.
  so (Hsur x Hx) as (y & Hxy & Hy & Heq).
  exists y.
  do2 2 split; auto.
  omega.
  }
omega.
Qed.

Lemma weight_map_inj :
  forall S T (g : S -> nat) (h : T -> nat) (P : S -> Prop) (Q : T -> Prop) (f : S -> T) p q,
    (forall x, P x -> Q (f x) /\ g x <= h (f x))
    -> (forall x y, P x -> P y -> f x = f y -> x = y)
    -> weight g P p
    -> weight h Q q
    -> p <= q.
Proof.
intros S T g h P Q f m n Hincl Hinj HcardP HcardQ.
apply (weight_corr_le S T g h P Q (fun x y => f x = y) m n); auto.
  {
  intros x x' y Hx Hx' Hy Heq Heq'.
  apply Hinj; auto.
  transitivity y; auto.
  }

  {
  intros x Hx.
  so (Hincl x Hx) as (Hy & Hle).
  exists (f x).
  do2 2 split; auto.
  }
Qed.

Lemma weight_map_surj :
  forall S T (g : S -> nat) (h : T -> nat) (P : S -> Prop) (Q : T -> Prop) (f : T -> S) p q,
    (forall x, Q x -> P (f x) /\ g (f x) <= h x)
    -> (forall x, P x -> exists y, Q y /\ x = f y)
    -> weight g P p
    -> weight h Q q
    -> p <= q.
Proof.
intros S T g h P Q f m n Hincl Hsurj HcardP HcardQ.
apply (weight_corr_le S T g h P Q (fun x y => x = f y) m n); auto.
  {
  intros x x' y Hx Hx' Hy Heq Heq'.
  transitivity (f y); auto.
  }

  {
  intros x Hx.
  so (Hsurj x Hx) as (y & Hy & Heq).
  subst x.
  exists y.
  do2 2 split; auto.
  exact (Hincl _ Hy ander).
  }
Qed.

Lemma weight_incl :
  forall T (f : T -> nat) (P Q : T -> Prop) p q,
    incl P Q
    -> weight f P p
    -> weight f Q q
    -> p <= q.
Proof.
intros T f P Q p q HPQ Hp Hq.
eapply weight_map_inj with (f := (fun x => x)) (P := P) (Q := Q); eauto.
Qed.

(* Strange that these aren't in the library *)

Lemma fold_right_map :
  forall S T U (f : S -> T) (g : T -> U -> U) (l : list S) (x : U),
    fold_right g x (map f l) = fold_right (fun y z => g (f y) z) x l.
Proof.
intros S T U f g l x.
induct l; auto.
(* cons *)
intros y l IH.
cbn.
rewrite -> IH.
reflexivity.
Qed.

Lemma fold_right_ext_in :
  forall T U (f f' : T -> U -> U) (l : list T) (x : U),
    (forall y z, In y l -> f y z = f' y z)
    -> fold_right f x l = fold_right f' x l.
Proof.
intros T U f f' l x.
induct l; auto.
(* cons *)
intros y l IH Hext.
cbn.
rewrite <- IH.
  {
  apply Hext.
  left; auto.
  }

  {
  intros t u Ht.
  apply Hext.
  right; auto.
  }
Qed.

Lemma weight_image :
  forall S T (g : S -> nat) (h : T -> nat) (P : S -> Prop) (f : S -> T) n,
    (forall x, P x -> g x = h (f x))
    -> (forall x y, P x -> P y -> f x = f y -> x = y)
    -> weight g P n
    -> weight h (fun x => exists y, x = f y /\ P y) n.
Proof.
intros S T g h P f n Hwt Hinj HcardP.
destruct HcardP as (p & Hdistp & Hp & Hlenp).
exists (map f p).
do2 2 split.
  {
  so (fun x => Hp x ander) as H.
  revert H.
  clear Hp Hlenp.
  induct Hdistp.
    (* nil *)
    {
    intros _.
    apply NoDup_nil.
    }

    (* cons *)
    {
    intros x p Hnin _ IH Hp.
    cbn.
    apply NoDup_cons.
      {
      contradict Hnin.
      so (in_map_iff _#5 andel Hnin) as (x' & Heq & Hx').
      force_exact Hx'.
      f_equal.
      apply Hinj; auto.
        {
        apply Hp.
        right; auto.
        }

        {
        apply Hp.
        left; auto.
        }
      }

      {
      apply IH.
      intros y Hy.
      apply Hp.
      right; auto.
      }
    }
  }

  {
  intro x.
  split.
    {
    intros (y & -> & Hy).
    apply in_map.
    apply Hp; auto.
    }

    {
    intros Hx.
    so (in_map_iff _#5 andel Hx) as (y & <- & Hy).
    exists y.
    split; auto.
    apply Hp; auto.
    }
  }

  {
  unfold sumweight.
  rewrite -> fold_right_map.
  unfold sumweight in Hlenp.
  force_exact Hlenp.
  f_equal.
  apply fold_right_ext_in.
  intros y z Hy.
  f_equal.
  apply Hwt.
  apply Hp; auto.
  }
Qed.

Lemma weight_finite :
  forall T (f : T -> nat) (P : T -> Prop) n, weight f P n -> finite P.
Proof.
intros T f P n Hcard.
destruct Hcard as (l & _ & H & _).
exists l.
intros; apply H; auto.
Qed.

Lemma finite_weight :
  forall T (f : T -> nat) (P : T -> Prop),
    (forall (x y : T), decidable (x = y))
    -> finite P
    -> exists n, weight f P n.
Proof.
intros T f P Hdeceq Hfin.
destruct Hfin as (l & Hl).
so (deduplicate _ l Hdeceq) as (l' & Hdist & Hl').
exists (sumweight f l').
exists l'.
do2 2 split; auto.
intros x.
split.
  {
  intro Hx.
  apply Hl'.
  apply Hl; auto.
  }

  {
  intro Hx.
  apply Hl; auto.
  apply Hl'; auto.
  }
Qed.

Lemma weight_gt_decide :
  forall (T : Type) (f : T -> nat) (P U : T -> Prop) n n',
    (forall x, decidable (P x))
    -> incl P U
    -> weight f U n
    -> decidable (exists p, weight f P p /\ p > n').
Proof.
intros T f P U n n' Hdec HPU HcardU.
so HcardU as (u & Hdist & Hu & Hlenu).
so (enumerate_subset _#3 (fun x _ => Hdec x) Hdist) as (p & Hdistp & Hp).
so (le_lt_dec (sumweight f p) n') as [Hle | Hlt].
2:{
  left.
  exists (sumweight f p).
  split; auto.
  exists p.
  do2 2 split; auto.
  intros x.
  split.
    {
    intro Hx.
    apply Hp.
    split; auto.
    apply Hu.
    apply HPU; auto.
    }

    {
    intro Hx.
    apply Hp; auto.
    }
  }
right.
intro H.
destruct H as (m & HcardP & Hgt).
destruct HcardP as (p' & Hdistp' & Hp' & Hlenp).
exploit (permutation_weight' _ f p p') as Heq; auto.
  {
  intros x.
  split.
    {
    intro Hx.
    apply Hp'.
    apply Hp; auto.
    }

    {
    intro Hx.
    apply Hp.
    split.
      {
      apply Hp'; auto.
      }

      {
      apply Hu.
      apply HPU.
      apply Hp'; auto.
      }
    }
  }
omega.
Qed.

Definition weight_lt {T : Type} (f : T -> nat) (P : T -> Prop) (n : nat) : Prop
  :=
  ~ exists l,
      NoDup l
      /\ (forall x, In x l -> P x)
      /\ sumweight f l >= n.

Lemma weight_impl_weight_lt :
  forall T (f : T -> nat) (P : T -> Prop) m n,
    m < n
    -> weight f P m
    -> weight_lt f P n.
Proof.
intros T f P m n Hlt Hcard.
destruct Hcard as (k & Hdistk & Hk & Hlenk).
intros (l & Hdistl & Hl & Hlenl).
exploit (incl_weight _ f l k) as Hleq; auto.
  {
  intros x Hx.
  apply Hk.
  apply Hl; auto.
  }
omega.
Qed.

Lemma weight_lt_increase :
  forall T (f : T -> nat) (P : T -> Prop) m n,
    m <= n
    -> weight_lt f P m
    -> weight_lt f P n.
Proof.
intros T f P m n Hleq Hcard.
unfold weight_lt in *.
contradict Hcard.
destruct Hcard as (l & Hdist & Hl & Hlen).
exists l.
do2 2 split; auto.
omega.
Qed.

Lemma weight_lt_impl_lt :
  forall T (f : T -> nat) (P Q : T -> Prop) p q,
    incl P Q
    -> weight f P p
    -> weight_lt f Q q
    -> p < q.
Proof.
intros T f P Q p q HPQ Hp Hq.
so (lt_dec p q) as [| Hnlt]; auto.
exfalso.
assert (p >= q) as Hpq by omega.
destruct Hp as (l & Hdist & Hl & Hlen).
destruct Hq.
exists l.
do2 2 split; auto.
  {
  intros x Hx.
  apply HPQ.
  apply Hl; auto.
  }

  {
  omega.
  }
Qed.

Lemma weight_lt_by_contradiction :
  forall T (f : T -> nat) (P : T -> Prop) p,
    (forall Q q, incl Q P -> weight f Q q -> q >= p -> False)
    -> weight_lt f P p.
Proof.
intros T f P p Hprop.
intros (l & Hdist & Hl & Hlen).
apply (Hprop (fun x => In x l) (sumweight f l)); auto.
exists l.
do2 2 split; auto.
intro; split; auto.
Qed.

repo: coq-proof


text:
(* Require Import Toy.UnifySL.implementation. *)
Require Import ZArith.
Require Import QArith.
Require Import Toy.CC.lib.
Require Import Toy.CC.type.
Require Import Toy.CC.usl.implementation.
Import T.
Open Scope Z.

Module Denote_Aexp.

Definition add_sem (da1 da2 : state -> option Z) : state -> option Z :=
  fun st =>
    match da1 st, da2 st with
      | Some v1, Some v2 => Some (v1 + v2)
      | _, _ => None
    end.

Definition sub_sem (da1 da2 : state -> option Z) : state -> option Z :=
  fun st =>
    match da1 st, da2 st with
      | Some v1, Some v2 => Some (v1 - v2)
      | _, _ => None
    end.

Definition mul_sem (da1 da2 : state -> option Z) : state -> option Z :=
  fun st =>
    match da1 st, da2 st with
      | Some v1, Some v2 => Some (v1 * v2)
      | _, _ => None
    end.

Definition div_sem (da1 da2 : state -> option Z) : state -> option Z :=
  fun st =>
    match da1 st, da2 st with
      | Some v1, Some v2 =>
          if Z.eq_dec v2 0 then None else Some (v1 / v2)
      | _, _ => None
    end.

Definition deref_sem (da : state -> option Z) : state -> option Z :=
  fun st => match da st with
    | Some p => match snd st p with
      | Some (inl (q, v)) => if (Qlt_le_dec 0%Q q) then Some v else None
      | _ => None
    end
    | _ => None
  end.

Fixpoint aeval (a : aexp) : state -> option Z :=
  match a with
    | ANum n => fun _ =>  Some n
    | AId X => fun st => Some (fst st X)
    | APlus a1 a2 => add_sem (aeval a1) (aeval a2)
    | AMinus a1 a2 => sub_sem (aeval a1) (aeval a2)
    | AMult a1 a2 => mul_sem (aeval a1) (aeval a2)
    | ADiv a1 a2 => div_sem (aeval a1) (aeval a2)
    | ADeref a => deref_sem (aeval a)
  end.

End Denote_Aexp.

Definition opt_test (R : Z -> Z -> Prop) (X Y : state -> option Z) : bexp_denote :=
{|
  true_set := fun st =>
    match X st, Y st with
      | Some n1, Some n2 => R n1 n2
      | _, _ => False
    end;
  false_set := fun st =>
    match X st, Y st with
      | Some n1, Some n2 => ~ R n1 n2
      | _, _ => False
    end;
  error_set := fun st =>
    match X st, Y st with
      | Some n1, Some n2 => False
      | _, _ => True
    end; |}.

Module Denote_Bexp.
Import Denote_Aexp.

Fixpoint beval (b : bexp) : bexp_denote :=
  match b with
    | BTrue =>
        {| true_set := Sets.full;
           false_set := Sets.empty;
           error_set := Sets.empty; |}
    | BFalse =>
        {| true_set := Sets.empty;
           false_set := Sets.full;
           error_set := Sets.empty; |}
    | BEq a1 a2 =>
        opt_test Z.eq (aeval a1) (aeval a2)
    | BLe a1 a2 =>
        opt_test Z.le (aeval a1) (aeval a2)
    | BNot b =>
        {| true_set := false_set (beval b);
           false_set := true_set (beval b);
           error_set := error_set (beval b); |}
    | BAnd b1 b2 =>
        {| true_set := Sets.intersect (true_set (beval b1)) (true_set (beval b2));
           false_set := Sets.union (false_set (beval b1))
                                   (Sets.intersect (true_set (beval b1))
                                                   (false_set (beval b2)));
           error_set := Sets.union (error_set (beval b1))
                                   (Sets.intersect (true_set (beval b1))
                                                   (error_set (beval b2))); |}
       end.

End Denote_Bexp.

Module Denote_Term.
Import Denote_Aexp.

Definition add_term (a b : option Z) : option Z :=
  match a, b with
  | Some n1, Some n2 => Some (n1 + n2)
  | _, _ => None
  end.

Definition sub_term (a b : option Z) : option Z :=
  match a, b with
  | Some n1, Some n2 => Some (n1 - n2)
  | _, _ => None
  end.

Definition mul_term (a b : option Z) : option Z :=
  match a, b with
  | Some n1, Some n2 => Some (n1 * n2)
  | _, _ => None
  end.

Definition div_term (a b : option Z) : option Z :=
  match a, b with
  | Some n1, Some n2 => if (Z.eq_dec n2 0) then None else Some (n1 / n2)
  | _, _ => None
  end.

Definition deref_term (a : option Z) (st : state) : option Z :=
  match a with
  | Some p => match snd st p with
    | Some (inl (q, z)) => Some z
    | _ => None
  end
  | _ => None
  end.

Fixpoint term_denote (t : term) : state -> option Z :=
  fun st => match t with
  | TNum n => Some n
  | TDenote a => aeval a st
  | TPlus t1 t2 => add_term (term_denote t1 st) (term_denote t2 st)
  | TMinus t1 t2 => sub_term (term_denote t1 st) (term_denote t2 st)
  | TMult t1 t2 => mul_term (term_denote t1 st) (term_denote t2 st)
  | TDiv t1 t2 => div_term (term_denote t1 st) (term_denote t2 st)
  | TDeref t => deref_term (term_denote t st) st
  end.

End Denote_Term.

Module Denote_Assertion_D.
Import Denote_Term.
Import Denote_Bexp.

Fixpoint Assertion_Denote (d : Assertion_D) (st : state) : Prop :=
  match d with
  | DLe t1 t2 => match (term_denote t1 st), (term_denote t2 st) with
    | Some n1, Some n2 => n1 <= n2
    | _, _ => False
  end
  | DLt t1 t2 => match (term_denote t1 st), (term_denote t2 st) with
    | Some n1, Some n2 => n1 < n2
    | _, _ => False
  end
  | DEq t1 t2 => match (term_denote t1 st), (term_denote t2 st) with
    | Some n1, Some n2 => n1 = n2
    | _, _ => False
  end
  | DInj b => true_set (beval b) st
  | DProp P => P
  | DOr d1 d2 => (Assertion_Denote d1 st) \/ (Assertion_Denote d2 st)
  | DAnd d1 d2 => (Assertion_Denote d1 st) /\ (Assertion_Denote d2 st)
  | DNot d => ~ (Assertion_Denote d st)
  | DMapsto pt vt => match (term_denote pt st), (term_denote vt st) with
    | Some p, Some v => match snd st p with
      | Some (inl (q, z)) => z = v
      | _ => False
    end
    | _, _ => False
  end
  | DHasLock L pi R => match snd st L with
    | Some (inr ((q, None), r)) => q = pi /\ r = R
    | _ => False
  end
  | DReadytoRel L pi R => match snd st L with
    | Some (inr ((q, Some tt), r)) => q = pi /\ r = R
    | _ => False
  end
  | DSepcon d1 d2 => exists st1 st2,
    (Assertion_Denote d1 st1) /\ (Assertion_Denote d2 st2) /\ stateJ st1 st2 st
end.

End Denote_Assertion_D.

Module Denote_Com.
Import Denote_Aexp.
Import Denote_Bexp.
Import Denote_Assertion_D.

Definition skip_sem : com_denote := {|
  com_normal := BinRel.id;
  com_break := BinRel.empty;
  com_cont := BinRel.empty;
  com_error := Sets.empty |}.

Definition break_sem : com_denote := {|
  com_normal := BinRel.empty;
  com_break := BinRel.id;
  com_cont := BinRel.empty;
  com_error := Sets.empty |}.

Definition cont_sem : com_denote := {|
  com_normal := BinRel.empty;
  com_break := BinRel.empty;
  com_cont := BinRel.id;
  com_error := Sets.empty |}.

Definition set_sem (X : var) (DA : state -> option Z): com_denote := {|
  com_normal := fun st1 st2 => match DA st1 with
    | Some v => fst st2 X = v /\ (forall Y, Y <> X -> fst st2 Y = fst st1 Y) /\ snd st2 = snd st1
    | _ => False
  end;
  com_break := BinRel.empty;
  com_cont := BinRel.empty;
  com_error := fun st => DA st = None |}.

Definition store_sem (DAL DAR : state -> option Z) : com_denote := {|
  com_normal := fun st1 st2 => match (DAL st1), (DAR st1) with
    | Some p, Some v => match (snd st1 p), (snd st2 p) with
      | Some (inl (q1, z1)), Some (inl (q2, z2)) => q1 = 1%Q /\ q2 = 1%Q /\ z2 = v /\
          (forall p', p' <> p -> snd st2 p' = snd st1 p') /\ fst st1 = fst st2
      | _, _ => False
    end
    | _, _ => False
  end;
  com_break := BinRel.empty;
  com_cont := BinRel.empty;
  com_error := fun st => match (DAL st), (DAR st) with
    | Some p, Some v => match snd st p with
      | Some (inl (q, z)) => ~(Qeq q 1%Q)
      | _ => True
    end
    | _, _ => True
  end |}.

Definition seq_sem (DC1 DC2 : com_denote) : com_denote := {|
  com_normal := BinRel.concat (com_normal DC1) (com_normal DC2);
  com_break := BinRel.union (com_break DC1) (BinRel.concat (com_normal DC1) (com_break DC2));
  com_cont := BinRel.union (com_cont DC1) (BinRel.concat (com_normal DC1) (com_cont DC2));
  com_error := Sets.union (com_error DC1) (BinRel.dia (com_normal DC1) (com_error DC2)) |}.

Definition if_sem (DB : bexp_denote) (DC1 DC2 : com_denote) : com_denote := {|
  com_normal := BinRel.union (BinRel.concat (BinRel.testrel (true_set DB)) (com_normal DC1))
    (BinRel.concat (BinRel.testrel (false_set DB)) (com_normal DC2));
  com_break := BinRel.union (BinRel.concat (BinRel.testrel (true_set DB)) (com_break DC1))
    (BinRel.concat (BinRel.testrel (false_set DB)) (com_break DC2));
  com_cont := BinRel.union (BinRel.concat (BinRel.testrel (true_set DB)) (com_cont DC1))
    (BinRel.concat (BinRel.testrel (false_set DB)) (com_cont DC2));
  com_error := Sets.union (error_set DB)
    (Sets.union (Sets.intersect (true_set DB) (com_error DC1)) (Sets.intersect (false_set DB) (com_error DC2)))|}.

Fixpoint iter_loop_body (DC1 DC2 : com_denote) (n : nat) : com_denote := match n with
  | O => {|
      com_normal := BinRel.union (com_break DC1) (BinRel.concat (com_normal DC1) (com_break DC2));
      com_break := BinRel.empty;
      com_cont := BinRel.empty;
      com_error := Sets.union (com_error DC1) (BinRel.dia (com_normal DC1) (com_error DC2)) |}
  | S n' => {|
      com_normal := BinRel.concat
        (BinRel.union (BinRel.concat (com_normal DC1) (com_normal DC2))
          (BinRel.concat (com_cont DC1) (com_normal DC2)))
        (com_normal (iter_loop_body DC1 DC2 n'));
      com_break := BinRel.empty;
      com_cont := BinRel.empty;
      com_error := BinRel.dia
        (BinRel.union (BinRel.concat (com_normal DC1) (com_normal DC2))
          (BinRel.concat (com_cont DC1) (com_normal DC2)))
        (com_error (iter_loop_body DC1 DC2 n')) |}
end.

Definition for_sem (DC1 DC2 : com_denote) : com_denote := {|
  com_normal := BinRel.omega_union (fun n => com_normal (iter_loop_body DC1 DC2 n));
  com_break := BinRel.empty;
  com_cont := BinRel.empty;
  com_error := Sets.omega_union (fun n => com_error (iter_loop_body DC1 DC2 n)) |}.

Definition new_sem (X : var) : com_denote := {|
  com_normal := fun st1 st2 =>
    exists p, fst st2 X = p /\ snd st1 p = None /\ snd st2 p = Some (inl (1%Q, 0)) /\
      (forall p', p' <> p -> snd st2 p = snd st1 p) /\
      (forall Y, Y <> X -> fst st2 Y = fst st1 Y);
  com_break := BinRel.empty;
  com_cont := BinRel.empty;
  com_error := Sets.empty |}.

Definition delete_sem (X : var) : com_denote := {|
  com_normal := fun st1 st2 => match fst st1 X with
    | p => exists z, snd st1 p = Some (inl (1%Q, z)) /\ snd st2 p = None /\
        (forall p', p' <> p -> snd st2 p' = snd st1 p') /\ fst st1 = fst st2
  end;
  com_break := BinRel.empty;
  com_cont := BinRel.empty;
  com_error := fun st => match snd st (fst st X) with
    | Some (inl (q, z)) => ~(Qeq q 1%Q)
    | _ => True
  end |}.

Definition mapsto_sem (st : state) (p : addr) (v : Z) (pi : Q) :=
  snd st p = Some (inl (pi, v)) /\ (forall p', p' <> p -> snd st p = None).

Definition mapsto__sem (st : state) (p : addr) (pi : Q) :=
  exists v, snd st p = Some (inl (pi, v)) /\ (forall p', p' <> p -> snd st p = None).

Definition hasLock_sem (st : state) (l : addr) (pi : Q) (P : Assertion_D) :=
  snd st l = Some (inr (pi, None, P)) /\ (forall p', p' <> l -> snd st p' = None).

Definition readytoRelease_sem (st : state) (l : addr) (pi : Q) (P : Assertion_D) :=
  snd st l = Some (inr (pi, Some tt, P)) /\ (forall p', p' <> l -> snd st p' = None).

Definition emp_sem (st : state) := forall p, snd st p = None.

Definition heap_Update (h : heap) (p : addr) v : heap :=
  fun p' => if (Z.eq_dec p' p) then v else h p'.

Definition make_sem (l : addr) (P Q : Assertion_D) : com_denote := {|
  com_normal := fun st1 st2 => exists st11 st12 st121 st122 st21 st22,
    stateJ st11 st12 st1 /\ stateJ st121 st122 st12 /\ stateJ st21 st22 st2 /\
    Assertion_Denote P st11 /\ Assertion_Denote Q st121 /\ mapsto__sem st122 l 1%Q /\
    Assertion_Denote Q st21 /\ hasLock_sem st22 l 1%Q P;
  com_break := BinRel.empty;
  com_cont := BinRel.empty;
  com_error := fun st => ~ (exists st11 st12, stateJ st11 st12 st /\ Assertion_Denote P st11) \/
    snd st l = None |}.

Definition deallocate_sem (l : addr) : com_denote := {|
  com_normal := fun st1 st2 => match snd st1 l with
    | Some (inr (1%Q, None, P)) => exists st21 st22,
        stateJ st21 st22 st2 /\ Assertion_Denote P st21 /\ st22 = (fst st1, heap_Update (snd st1) l (Some (inl (1%Q, 0))))
    | _ => False
  end;
  com_break := BinRel.empty;
  com_cont := BinRel.empty;
  com_error := fun st => match snd st l with
    | Some (inr (1%Q, None, P)) => False
    | _ => True
  end |}.

Definition acquire_sem (l : addr) : com_denote := {|
  com_normal := fun st1 st2 => match snd st1 l with
    | Some (inr (q, none, P)) => exists st21 st22,
        stateJ st21 st22 st2 /\ Assertion_Denote P st21 /\ st22 = (fst st1, heap_Update (snd st1) l (Some (inr (q, Some tt, P))))
    | _ => False
  end;
  com_break := BinRel.empty;
  com_cont := BinRel.empty;
  com_error := fun st => match snd st l with
    | Some (inr (q, none, P)) => False
    | _ => True
  end |}.

Definition release_sem (l : addr) (Q' : Assertion_D) (pi : Q) : com_denote := {|
  com_normal := fun st1 st2 => exists st11 st12 st121 st122 st21 st22 P,
    stateJ st11 st12 st1 /\ stateJ st121 st122 st12 /\ stateJ st21 st22 st2 /\
    Assertion_Denote P st11 /\ Assertion_Denote Q' st121 /\ readytoRelease_sem st122 l pi P /\
    Assertion_Denote Q' st21 /\ hasLock_sem st22 l pi P;
  com_break := BinRel.empty;
  com_cont := BinRel.empty;
  com_error := fun st => match snd st l with
    | Some (inr (pi, Some tt, P)) => ~(exists st1 st2, stateJ st1 st2 st /\ Assertion_Denote P st1)
    | _ => True
  end |}.

(* Definition acquire_sem (p : addr) : com_denote := {|
  com_normal := fun st1 st2 => match snd st1 p with
    | Some (inr ((q, None), Q)) => Qlt 0%Q q /\ snd st2 p = Some (inr ((q, Some tt), Q)) /\
        (forall p', p' <> p -> snd st2 p = snd st1 p) /\ (fst st1 = fst st2)
    | _ => False
  end;
  com_break := BinRel.empty;
  com_cont := BinRel.empty;
  com_error := fun st => match snd st p with
    | Some (inr ((q, None), Q)) => q = 0%Q
    | _ => True
  end |}.

Definition release_sem (p : addr) : com_denote := {|
  com_normal := fun st1 st2 => match snd st1 p with
    | Some (inr ((q, Some tt), Q)) => snd st2 p = Some (inr ((q, None), Q)) /\
        (forall p', p' <> p -> snd st2 p = snd st1 p) /\ (fst st1 = fst st2)
    | _ => False
  end;
  com_break := BinRel.empty;
  com_cont := BinRel.empty;
  com_error := fun st => match snd st p with
    | Some (inr ((q, Some tt), Q)) => False
    | _ => True
  end |}. *)

Fixpoint ceval (c : com) : com_denote :=
  match c with
  | CSkip => skip_sem
  | CBreak => break_sem
  | CCont => cont_sem
  | CSet X a => set_sem X (aeval a)
  | CStore a1 a2 => store_sem (aeval a1) (aeval a2)
  | CSeq c1 c2 => seq_sem (ceval c1) (ceval c2)
  | CIf b c1 c2 => if_sem (beval b) (ceval c1) (ceval c2)
  | CFor c1 c2 => for_sem (ceval c1) (ceval c2)
  | CNew X => new_sem X
  | CDelete X => delete_sem X
  | CMake l P Q => make_sem l P Q
  | CAcquire p => acquire_sem p
  | CRelease p Q pi => release_sem p Q pi
  | CDeallocate p => deallocate_sem p
  end.

End Denote_Com.

repo: Toy-Language-Address