text:
(*|
############################################################
Formalizing STLC with Tealeaves
############################################################
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Algebraic presentation
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

This file gives a tutorial on proving the decorated traversable monad
laws the for the syntax of the simply-typed lambda calculus (STLC).

.. contents:: Table of Contents
   :depth: 2

============================
Imports and setup
============================

Since we are using the algebraic typeclass hierarchy, we import modules under
the namespaces ``Classes.Algebraic`` and ``Theory.Algebraic.``
|*)

From Tealeaves Require Export
  Classes.DT.Monad
  Classes.Monoid
  Classes.Listable.Functor
  Data.Natural.

Import Traversable.Functor.Notations.
Import List.ListNotations.
Import Strength.Notations.
Import Monoid.Notations.

#[local] Generalizable All Variables.
#[local] Set Implicit Arguments.

(*|
=====================
Language Definition
=====================

The first step with Tealeaves is to define the syntax of the
language. We take a type ``base_typ`` of types we consider primitive
(a/k/a atomic). The set of simple types is built up by forming arrows
between types, starting with base types. The syntax of STLC is defined
with three constructors as usual.
|*)

Parameter base_typ : Type.

Inductive typ :=
| base : base_typ -> typ
| arr : typ -> typ -> typ.

Coercion base : base_typ >-> typ.

(* we give more informative names to [Lam]'s arguments
 than Coq would infer otherwise *)
Inductive term (A : Type) :=
| Var : A -> term A
| Lam : forall (X : typ) (t : term A), term A
| Ap : term A -> term A -> term A.

Module Notations.
  Notation "'λ' X ⋅ body" :=
    (Lam X body) (at level 45) : tealeaves_scope.
  Notation "[ t1 ] [ t2 ]" :=
    (Ap t1 t2) (at level 40) : tealeaves_scope.
  Notation "A ⟹ B" :=
    (arr A B) (at level 40) : tealeaves_scope.
End Notations.

Import Notations.

(*|
For convenience, we define an extremely rudimentary Ltac tactic that
will solve the most trivial inductive steps automatically. Namely,
they will attempt to solve a goal in one step by rewriting with the
hypotheses in context (up to two times), then calling ``reflexivity``.
|*)

Ltac basic t :=
  induction t;
  [ reflexivity |
    simpl; match goal with H : _ |- _ => rewrite H end; reflexivity |
    simpl; do 2 match goal with H : _ |- _ => rewrite H end; reflexivity ].

(*|
=====================
Functor instances
=====================

Plain Functor instance
========================

Note that our datatype ``term`` is parameterized by a single type
variable. The first thing we must show is that ``term`` is actually
*functor* in this type argument.
|*)

Fixpoint fmap_term {A B : Type} (f : A -> B) (t : term A) : term B :=
  match t with
  | Var a => Var (f a)
  | Lam X t => Lam X (fmap_term f t)
  | Ap t1 t2 => Ap (fmap_term f t1) (fmap_term f t2)
  end.

#[export] Instance Fmap_term : Fmap term := @fmap_term.

Theorem fmap_id : forall A, fmap term id = @id (term A).
Proof.
  intros. ext t. unfold transparent tcs. basic t.
Qed.

Theorem fmap_fmap : forall A B C (f : A -> B) (g : B -> C),
    fmap term g ∘ fmap term f = fmap term (g ∘ f).
Proof.
  intros. ext t. unfold transparent tcs.
  unfold compose. basic t.
Qed.

#[export] Instance Functor_term : Functor term :=
  {| fun_fmap_id := @fmap_id;
     fun_fmap_fmap := @fmap_fmap;
  |}.

(*|
Rewriting rules for ``fmap``
-----------------------------
|*)

Section fmap_term_rewrite.

  Context
    `{f : A -> B}.

  Lemma fmap_term_ap : forall (t1 t2 : term A),
      fmap term f (@Ap A t1 t2) = @Ap B (fmap term f t1) (fmap term f t2).
  Proof.
    reflexivity.
  Qed.

End fmap_term_rewrite.

(*|
Decorated Functor instance
===========================
|*)

Fixpoint dec_term {A} (t : term A) : term (nat * A) :=
  match t with
  | Var a => Var (Ƶ, a)
  | Lam τ t => Lam τ (shift term (1, dec_term t))
  | Ap t1 t2 => Ap (dec_term t1) (dec_term t2)
  end.

#[export] Instance Decorate_term : Decorate nat term := @dec_term.

Theorem dec_natural : forall A B (f : A -> B),
    fmap term (fmap (prod nat) f) ∘ dec term = dec term ∘ fmap term f.
Proof.
  intros. unfold compose. ext t. induction t.
  - now cbn.
  - cbn -[shift]. fequal. now rewrite dec_helper_1.
  - cbn. now fequal.
Qed.

#[export] Instance: Natural (@dec nat term _).
Proof.
  constructor.
  - typeclasses eauto.
  - apply Functor_compose.
  - apply dec_natural.
Qed.

Theorem dec_extract : forall A,
    fmap term (extract (prod nat)) ∘ dec term = @id (term A).
Proof.
  intros. unfold compose. ext t. induction t.
  - reflexivity.
  - cbn -[shift]. now rewrite dec_helper_2.
  - unfold id. cbn. now fequal.
Qed.

Theorem dec_dec : forall A,
    dec term ∘ dec term = fmap term (cojoin (prod nat)) ∘ dec term (A := A).
Proof.
  intros. unfold compose. ext t. induction t.
  - reflexivity.
  - cbn -[shift]. fequal. now rewrite dec_helper_3.
  - cbn. fequal; auto.
Qed.

#[export] Instance DecoratedFunctor_term : DecoratedFunctor nat term.
Proof.
  constructor.
  - typeclasses eauto.
  - typeclasses eauto.
  - apply dec_dec.
  - apply dec_extract.
Qed.

(*|
Rewriting rules for ``dec``
-----------------------------
|*)

Section dec_term_rewrite.

  Context
    `{f : A -> B}.

  Lemma dec_term1 : forall (x : A),
      dec term (Var x) = Var (0, x).
  Proof.
    reflexivity.
  Qed.

  Lemma dec_term21 : forall (X : typ) (t : term A),
      dec term (Lam X t) = shift term (1, Lam X (dec term t)).
  Proof.
    reflexivity.
  Qed.

  Lemma dec_term22 : forall (X : typ) (t : term A),
      dec term (Lam X t) = Lam X (shift term (1, dec term t)).
  Proof.
    reflexivity.
  Qed.

  Lemma dec_term3 : forall (t1 t2 : term A),
      dec term (Ap t1 t2) = Ap (dec term t1) (dec term t2).
  Proof.
    reflexivity.
  Qed.

End dec_term_rewrite.

(*|
Traversable Functor instance
==============================
|*)

Import Applicative.Notations.

Fixpoint dist_term `{Fmap F} `{Pure F} `{Mult F} {A : Type}
         (t : term (F A)) : F (term A) :=
  match t with
  | Var a => fmap F (@Var A) a
  | Lam X t => fmap F (Lam X) (dist_term t)
  | Ap t1 t2 => (pure F (@Ap A))
                 <⋆> dist_term t1
                 <⋆> dist_term t2
  end.

#[export] Instance: Dist term := @dist_term.

(*|
Rewriting rules for ``dist``
-----------------------------
|*)

Section term_dist_rewrite.

  Context
    `{Applicative G}.

  Variable (A : Type).

  Lemma dist_term_var_1 : forall (x : G A),
    dist term G (@Var (G A) x) = pure G (@Var A) <⋆> x.
  Proof.
    intros. cbn. now rewrite fmap_to_ap.
  Qed.

  Lemma dist_term_var_2 : forall (x : G A),
    dist term G (@Var (G A) x) = fmap G (@Var A) x.
  Proof.
    reflexivity.
  Qed.

  Lemma dist_term_lam_1 : forall (X : typ) (t : term (G A)),
      dist term G (Lam X t) = pure G (Lam X) <⋆> (dist term G t).
  Proof.
    intros. cbn. now rewrite fmap_to_ap.
  Qed.

  Lemma dist_term_lam_2 : forall (X : typ) (t : term (G A)),
      dist term G (Lam X t) = fmap G (Lam X) (dist term G t).
  Proof.
    reflexivity.
  Qed.

  Lemma dist_term_ap_1 : forall (t1 t2 : term (G A)),
      dist term G (Ap t1 t2) =
      (pure G (@Ap A))
        <⋆> dist term G t1
        <⋆> dist term G t2.
  Proof.
    reflexivity.
  Qed.

  Lemma dist_term_ap_2 : forall (t1 t2 : term (G A)),
      dist term G (Ap t1 t2) =
      (fmap G (@Ap A) (dist term G t1)
            <⋆> dist term G t2).
  Proof.
    intros. rewrite dist_term_ap_1.
    now rewrite fmap_to_ap.
  Qed.

End term_dist_rewrite.

Section dist_term_properties.

  Context
    `{Applicative G}.

(*|
Naturality of ``dist``
-----------------------------
|*)

  Lemma dist_natural_term : forall `(f : A -> B),
      fmap (G ∘ term) f ∘ dist term G =
      dist term G ∘ fmap (term ∘ G) f.
  Proof.
    intros; cbn. ext t.
    unfold_ops @Fmap_compose. unfold compose. induction t.
    + cbn. compose near a. now rewrite 2(fun_fmap_fmap G).
    + cbn. rewrite <- IHt.
      compose near (dist term G t).
      now rewrite 2(fun_fmap_fmap G).
    + rewrite (dist_term_ap_2).
      rewrite (fmap_term_ap).
      rewrite (dist_term_ap_2).
      rewrite <- IHt1, <- IHt2.
      rewrite <- ap_fmap.
      rewrite fmap_ap. fequal.
      compose near (dist term G t1).
      rewrite (fun_fmap_fmap G).
      rewrite (fun_fmap_fmap G).
      compose near (dist term G t1) on right.
      rewrite (fun_fmap_fmap G).
      reflexivity.
  Qed.

  #[export] Instance dist_Natural_term :
      Natural (@dist term _ _ _ _ _).
  Proof.
    intros. constructor.
    - typeclasses eauto.
    - typeclasses eauto.
    - intros. apply dist_natural_term.
  Qed.

(*|
Traversal laws
-----------------------------
|*)

  Lemma dist_unit_term : forall (A : Type),
      dist term (fun A => A) = @id (term A).
  Proof.
    intros. ext t. induction t.
    - reflexivity.
    - cbn. rewrite IHt. reflexivity.
    - cbn. rewrite IHt1, IHt2.
      reflexivity.
  Qed.

  #[local] Set Keyed Unification.
  Lemma dist_linear_term : forall `{Applicative G1} `{Applicative G2} (A : Type),
      dist term (G1 ∘ G2) =
      fmap G1 (dist term G2) ∘ dist term G1 (A := G2 A).
  Proof.
    intros. unfold compose. ext t. induction t.
    - cbn. compose near a on right. now rewrite (fun_fmap_fmap G1).
    - cbn. rewrite IHt. compose near (dist term G1 t).
      change (fmap (G1 ○ G2) (Lam X)) with (fmap G1 (fmap G2 (@Lam A X))).
      rewrite (fun_fmap_fmap G1).
      now rewrite (fun_fmap_fmap G1).
    - rewrite dist_term_ap_2.
      rewrite (dist_term_ap_2 (G := G1 ○ G2)).
      rewrite fmap_ap.
      compose near ((dist term G1 t1)).
      rewrite (fun_fmap_fmap G1).
      rewrite (ap_compose2 G2 G1).
      rewrite IHt1, IHt2.
      rewrite <- ap_fmap. fequal.
      repeat (compose near (dist term G1 t1) on left;
              rewrite (fun_fmap_fmap G1)).
      fequal. ext s1 s2. unfold compose; cbn.
      unfold precompose. now rewrite (fmap_to_ap).
  Qed.
  #[local] Unset Keyed Unification.

  Lemma dist_morph_term : forall `{ApplicativeMorphism G1 G2 ϕ} A,
      dist term G2 ∘ fmap term (ϕ A) = ϕ (term A) ∘ dist term G1.
  Proof.
    intros. ext t. unfold compose. induction t.
    - cbn. now rewrite <- (appmor_natural G1 G2).
    - cbn. rewrite IHt.
      now rewrite (appmor_natural G1 G2).
    - rewrite fmap_term_ap. inversion H9.
      rewrite dist_term_ap_2.
      rewrite IHt1. rewrite IHt2.
      rewrite dist_term_ap_2. rewrite (ap_morphism_1).
      fequal. now rewrite <- (appmor_natural).
  Qed.

End dist_term_properties.

#[export] Instance TraversableFunctor_term : TraversableFunctor term :=
  {| dist_natural := @dist_Natural_term;
     dist_morph := @dist_morph_term;
     dist_linear := @dist_linear_term;
     dist_unit := @dist_unit_term;
  |}.

(*|
Decorated-Traversable Functor instance
=======================================
|*)

Lemma dtfun_compat_term1 : forall `{Applicative G} (X : typ) {A},
    fmap G (dec term ∘ Lam X) ∘ δ term G (A := A) =
    fmap G (curry (shift term) 1 ∘ Lam X) ∘ fmap G (dec term) ∘ δ term G.
Proof.
  intros. rewrite (fun_fmap_fmap G). reflexivity.
Qed.

Theorem dtfun_compat_term :
        `(forall `{Applicative G} {A : Type},
             dist term G ∘ fmap term (strength G) ∘ dec term (A := G A) =
             fmap G (dec term) ∘ dist term G).
Proof.
  intros. ext t. unfold compose. induction t.
  - cbn. compose near a. now rewrite 2(fun_fmap_fmap G).
  - cbn. do 2 (compose near (dec term t) on left;
               rewrite (fun_fmap_fmap term)).
    reassociate <-. rewrite (strength_shift1 nat G).
    rewrite <- (fun_fmap_fmap term); unfold compose.
    change (fmap term (fmap G ?f)) with (fmap (term ∘ G) f).
    compose near ((fmap term (σ G) (dec term t))).
    unfold_compose_in_compose.
    rewrite <- (natural (ϕ := @dist term _ G _ _ _)).
    unfold compose.
    rewrite IHt. compose near (δ term G t).
    rewrite (fun_fmap_fmap G).
    compose near (δ term G t) on left.
    unfold_ops @Fmap_compose; rewrite 2(fun_fmap_fmap G).
    fequal. ext t'; unfold compose; cbn.
    compose near (dec term t') on right; now rewrite (fun_fmap_fmap term).
  - cbn. rewrite IHt1, IHt2. rewrite fmap_ap. rewrite fmap_ap.
    rewrite pure_ap_fmap. rewrite <- ap_fmap.
    rewrite (app_pure_natural G). rewrite <- (fmap_to_ap).
    compose near (δ term G t1) on left. rewrite (fun_fmap_fmap G).
    reflexivity.
Qed.

#[export] Instance : DecoratedTraversableFunctor nat term :=
  {| dtfun_compat := @dtfun_compat_term |}.

(*|
=====================
Monad instances
=====================

Plain Monad instance
=====================
|*)

Fixpoint join_term {A : Type} (t : term (term A)) : term A :=
  match t with
  | Var t' => t'
  | Lam X t => Lam X (join_term t)
  | Ap t1 t2 => Ap (join_term t1) (join_term t2)
  end.

#[export] Instance Ret_term : Return term := @Var.

#[export] Instance Join_term : Join term := @join_term.

Theorem ret_natural : forall A B (f : A -> B),
    fmap term f ∘ ret term = ret term ∘ f.
Proof.
  reflexivity.
Qed.

Theorem join_natural : forall A B (f : A -> B),
    fmap term f ∘ join term = join term ∘ fmap term (fmap term f).
Proof.
  intros. ext t. unfold transparent tcs.
  unfold compose. basic t.
Qed.

#[export] Instance: Natural (@ret term _).
Proof.
  constructor; try typeclasses eauto.
  apply ret_natural.
Qed.

#[export] Instance: Natural (@join term _).
Proof.
  constructor.
  - typeclasses eauto.
  - typeclasses eauto.
  - apply join_natural.
Qed.

Theorem join_ret : forall A,
    join term ∘ ret term = @id (term A).
Proof.
  reflexivity.
Qed.

Theorem join_fmap_ret : forall A,
    join term ∘ fmap term (ret term) = @id (term A).
Proof.
  intros. unfold compose. unfold transparent tcs.
  ext t. basic t.
Qed.

Theorem join_join : forall A,
    join term ∘ join term = join term (A := A) ∘ fmap term (join term).
Proof.
  intros. unfold compose. unfold transparent tcs.
  ext t. basic t.
Qed.

#[export] Instance Monad_term : Monad term :=
  {| mon_join_ret := join_ret;
     mon_join_fmap_ret := join_fmap_ret;
     mon_join_join := join_join |}.

(*|
Decorated Monad instance
===========================
|*)

Theorem dec_ret : forall A,
    dec term ∘ ret term (A := A) = ret term ∘ pair Ƶ.
Proof.
  reflexivity.
Qed.

Theorem dec_join : forall A,
    dec term ∘ join term (A := A) =
    join term ∘ fmap term (shift term) ∘ dec term ∘ fmap term (dec term).
Proof.
  intros. unfold compose. ext t. induction t.
  - cbn -[shift]. now rewrite (shift_zero term).
  - cbn -[shift]. fequal. now rewrite (dec_helper_4).
  - cbn. fequal; auto.
Qed.

#[export] Instance DecoratedMonad_term : DecoratedMonad nat term.
Proof.
  constructor.
  - typeclasses eauto.
  - typeclasses eauto.
  - typeclasses eauto.
  - apply dec_ret.
  - apply dec_join.
Qed.

(*|
Traversable Monad instance
==============================
|*)

Theorem trvmon_ret_term `{Applicative G} :
  `(dist term G ∘ ret term (A := G A) = fmap G (ret term)).
Proof.
  intros. ext x. reflexivity.
Qed.

#[local] Set Keyed Unification.
Theorem trvmon_join_term `{Applicative G} :
  `(dist term G ∘ join term = fmap G (join term) ∘ dist (term ∘ term) G (A := A)).
Proof.
  intros. ext t. unfold compose. induction t.
  - cbn. compose near (dist term G a).
    rewrite (fun_fmap_fmap G).
    replace (join term ∘ Var (A := term A)) with (@id (term A)).
    now rewrite (fun_fmap_id G).
    apply (join_ret).
  - cbn. rewrite IHt.
    unfold_ops @Dist_compose. unfold compose.
    compose near (dist term G (fmap term (dist term G) t)).
    rewrite (fun_fmap_fmap G).
    rewrite (fun_fmap_fmap G).
    reflexivity.
  - cbn. rewrite IHt1, IHt2.
    unfold_ops @Dist_compose. unfold compose.
    rewrite <- fmap_to_ap.
    rewrite <- fmap_to_ap.
    rewrite <- ap_fmap. rewrite fmap_ap.
    fequal. compose near ((dist term G (fmap term (dist term G) t1))).
    repeat rewrite (fun_fmap_fmap G).
    compose near ((dist term G (fmap term (dist term G) t1))) on left.
    rewrite (fun_fmap_fmap G).
    fequal.
Qed.
#[local] Set Keyed Unification.

#[export] Instance TraversableMonad_term : TraversableMonad term :=
  {| trvmon_ret := @trvmon_ret_term;
     trvmon_join := @trvmon_join_term;
  |}.

(*|
Decorated-Traversable Monad instance
=======================================

Our hard work has paid off---a DTM is defined as the combination of the typeclass instances we have
given so far, so we can let Coq infer the DTM instance for us.
|*)

#[export] Instance : DecoratedTraversableMonad nat term := {}.

author: dunnl

repo: tealeaves

save_path: github-repos/coq/dunnl-tealeaves


text:
Require Import List.
Require Import ssreflect.

Variable A : Set.
Variable f : A -> bool.

Inductive prefix : list A -> list A -> Prop :=
 | prefix_nil : forall l, prefix nil l
 | prefix_next : forall (a: A) l l', prefix l l' -> prefix (a :: l) (a :: l').

Fixpoint filter (l : list A) : list A :=
  match l with
    | nil => nil
    | h :: t  => if (f h) then (h :: (filter t)) else (filter t)
  end.

Lemma filter_prefix : forall l l', prefix l (filter l') -> exists l0, prefix l0 l' /\ filter l0 = l.
Proof.
 move => l l'; move: l' l.
 elim => [l' H|a l' IH].
 - by exists nil; rewrite /= in H; inversion H; split; [ apply prefix_nil | done ].
 - case => [|a' l].
   * by exists nil; split; [ apply prefix_nil | done ].
   * rewrite /=; case H: (f a) => H0.
     + inversion H0 as [|a0 l0 l'0 H1 [H2 H4] [H3 H5]].
       pose proof (IH l) as H6.
       apply H6 in H1.
       elim: H1 => l1 H1 {H6}.
       elim: H1 => H1 H6.
       exists (a :: l1); split.
       - by apply prefix_next.
       - by rewrite /=; case H7: (f a); [ rewrite H6 | rewrite H in H7 ].
     + pose proof (IH (a' :: l)) as H1.
       apply H1 in H0.
       elim: H0 => l0 H2 {H1}.
       elim: H2 => H2 H3.
       exists (a :: l0); split.
       - by apply prefix_next.
       - by rewrite /=; case H4: (f a); [ rewrite H in H4 | rewrite H3 ].
Qed.

author: palmskog

repo: pcc

save_path: github-repos/coq/palmskog-pcc


text:
Require Import all_ssreflect core.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Module Floyd_Warshall_Reachability.
Section Floyd_Warshall_Reachability.

Variable (T : finType).

Definition G := {ffun T * T -> bool}.

Definition floyd_warshall_zero (g : G) : G :=
  [ffun xy => (xy.1 == xy.2) || g xy].

Definition floyd_warshall_succ (g : G) (y : T) : G :=
  [ffun xz => let '(x, z) := xz in (g (x, y) && g (y, z)) || g (x, z)].

Definition connect (g : G) (P : pred T) (x y : T) :=
  [|| g (x, y), (x == y) |
    [exists y', connect (fun a b => P b && g (a, b)) x y' && g (y', y)]].

Lemma invariant_zero (g : G) :
  prod_uncurry (floyd_warshall_zero g) =2 connect g pred0.
Proof.
move=> x y; rewrite /prod_uncurry /floyd_warshall_zero /connect !ffunE /= orbC.
case_eq (g (x, y)); case: (altP (x =P y)) => //= Hxy1 /negbT Hxy2.
by apply/esym/existsP => -[y'] /andP [] /connectP [] [] //= _ ->; apply/negP.
Qed.

Lemma invariant_succ (g : G) P y :
  prod_uncurry g =2 connect g P ->
  prod_uncurry (floyd_warshall_succ g y) =2 connect g (predU1 y P).
Proof.
rewrite /prod_uncurry => /= H x z.
rewrite /floyd_warshall_succ /connect ffunE orbC.
case_eq (g (x, z)) => //= /negbT.
rewrite H /connect !negb_or negb_exists => /and3P [] H0 H1 _.
rewrite (negbTE H1) /=; apply/idP/existsP;
  [ case/andP; rewrite !H /connect => /or3P [] H2 /or3P [] H3 //= |
    case=> z' /andP [] /connectP [xs Hxs ->] H2].
- by exists y; rewrite H3 andbT;
     apply/connectP; exists [:: y] => //=; rewrite eqxx H2.
- by move/eqP: H3 H2 H0 => -> ->.
- by case/existsP: H3 => z' /andP [H3 H4]; exists z'; rewrite H4 andbT;
     case/connectP: H3 => ys H3 Hz'; subst z'; apply/connectP; exists (y :: ys);
     rewrite //= eqxx H2 /=; apply/sub_path: H3 => a b /andP [] -> ->;
     rewrite orbT.
- by move/eqP: H2 H3 H0 => -> ->.
- by move/eqP: H2 H3 H1 => -> ->.
- by move/eqP: H2 H3 => <- {y} /existsP [] z' /andP [H2 H3]; exists z';
     rewrite H3 andbT; apply/connect_sub: H2 => a b /andP [] H4 H5;
     apply/connect1; rewrite H4 H5 orbT.
- by exists y; rewrite {}H3 andbT;
     case/existsP: H2 => y' /andP [] /connectP [xs H2 Hy'] H3; subst y';
     apply/connectP; exists (rcons xs y);
     rewrite (rcons_path, last_rcons) //= eqxx H3 /= andbT;
     apply/sub_path: H2 => a b /andP [] -> ->; rewrite orbT.
- by move/eqP: H3 H2 => -> {y} /existsP [z'] /andP [] H2 H3; exists z';
     rewrite H3 andbT; apply/connect_sub: H2 => a b /andP [H4 H5];
     apply/connect1; rewrite H4 H5 orbT.
- by move: H2 H3 => /existsP [y'] /andP [] /connectP [xs] H2 -> {y'} H3
                    /existsP [z'] /andP [] /connectP [ys] H4 -> {z'} H5;
     exists (last y ys); rewrite H5 andbT; apply/connectP;
     exists (xs ++ y :: ys); rewrite (cat_path, last_cat) //= eqxx H3 /=;
     apply/andP; split; [move: H2 | move: H4];
     apply: sub_path => a b /andP [] -> ->; rewrite orbT.
(* shorten and splitting *)
-
Abort.

End Floyd_Warshall_Reachability.
End Floyd_Warshall_Reachability.

Module Floyd_Warshall.
Section Floyd_Warshall.

Variable (T : finType).

Definition G := {ffun T * T -> option nat}.

Definition add_distance (n m : option nat) : option nat :=
  match n, m with Some n', Some m' => Some (n' + m') | _, _ => None end.

Lemma add_distance_dN d : add_distance d None = None. Proof. by case: d. Qed.

Lemma add_distanceC : commutative add_distance.
Proof. by case=> [? |] [? |] //=; rewrite addnC. Qed.

Lemma add_distanceA : associative add_distance.
Proof. by case=> [? |] [? |] [? |] //=; rewrite addnA. Qed.

Definition lt_distance (n m : option nat) : bool :=
  match n, m with
    | None, _ => false
    | Some _, None => true
    | Some n', Some m' => n' < m'
  end.

Definition le_distance (n m : option nat) : bool := ~~ lt_distance m n.

Lemma lt_distance_d0 d : lt_distance d (Some 0) = false.
Proof. by case: d. Qed.

Lemma lt_distance_neq d1 d2 : lt_distance d1 d2 -> d1 != d2.
Proof.
by case: d1 d2 => [x |] [y |] => //= H;
   apply/eqP => -[H0]; move: H; rewrite H0 ltnn.
Qed.

Lemma lt_add_distanceL d1 d2 d3 :
  lt_distance (add_distance d1 d2) d3 -> lt_distance d1 d3.
Proof.
by case: d1 d2 d3 => [? |] [? |] [? |] => //=;
   apply: leq_trans; rewrite ltnS leq_addr.
Qed.

Lemma lt_add_distanceR d1 d2 d3 :
  lt_distance (add_distance d1 d2) d3 -> lt_distance d2 d3.
Proof. by rewrite add_distanceC; apply: lt_add_distanceL. Qed.

(*
Definition step (g : G) (x y : T) := if g (x, y) is Some _ then true else false.
*)

Definition floyd_warshall_zero (g : G) : G :=
  [ffun xy => let '(x, y) := xy in if x == y then Some 0 else g xy].

Definition floyd_warshall_succ (g : G) (y : T) : G :=
  [ffun xz =>
   let '(x, z) := xz in
   let xyz := add_distance (g (x, y)) (g (y, z)) in
   if lt_distance xyz (g (x, z)) then xyz else g (x, z)].

Definition m_floyd_warshall : AState {ffun T * T -> option nat} unit :=
  miterate_revfin' (fun i => astate_set (i, i) (Some 0));;
  miterate_revfin' (fun i =>
    miterate_revfin' (fun j =>
      mlet d_ji := astate_get (j, i) in
      if d_ji isn't Some dji then astate_ret tt else
      miterate_revfin' (fun k =>
        mlet d_ik := astate_get (i, k) in
        if d_ik isn't Some dik then astate_ret tt else
        mlet d_jk := astate_get (j, k) in
        if d_jk isn't Some djk then astate_set (j, k) (Some (dji + dik))
        else if djk <= dji + dik
             then astate_ret tt
             else astate_set (j, k) (Some (dji + dik))))).

End Floyd_Warshall.

Definition floyd_warshall (n : nat) (g : {ffun 'I_n * 'I_n -> option nat}) :
  {ffun 'I_n * 'I_n -> option nat} :=
  iterate_revfin
    (fun i => @floyd_warshall_succ [finType of 'I_n] ^~ i)
    (floyd_warshall_zero g).

Definition floyd_warshall_fast
           (n : nat) (g : {ffun 'I_n * 'I_n -> option nat}) :
  {ffun 'I_n * 'I_n -> option nat} :=
  (run_AState (m_floyd_warshall _) g).2.

End Floyd_Warshall.

Require Import extraction_ocaml.
Set Extraction Flag 8175.

Extraction Inline
  Floyd_Warshall.add_distance Floyd_Warshall.lt_distance
  Floyd_Warshall.floyd_warshall_zero Floyd_Warshall.floyd_warshall_succ
  Floyd_Warshall.m_floyd_warshall.

Extraction "../../ocaml/floyd_warshall.ml" Floyd_Warshall.

repo: efficient-finfun


text:
Module Type S.
  Parameter empty: Set.
End S.

Module D (M:S).
  Import M.
  Definition empty:=nat.
End D.

Module D' (M:S).
  Import M.
  Definition empty:Set. exact nat. Qed.
End D'.

author: princeton-vl

repo: CoqGym

save_path: github-repos/coq/princeton-vl-CoqGym


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

(****************************************************************************)
(*                                                                          *)
(*                  Binary Decision Trees (BDTs)                            *)
(*               MacMillan's "Proof" of canonicity of BDDs                  *)
(*                                                                          *)
(****************************************************************************)
(*                                  BDTs.v                                  *)
(****************************************************************************)

Require Import CanonBDDs.canonicite.Boolean_functions.
Require Import Vars.

Inductive BDT (n : nat) : Set :=
  | zero : BDT n
  | one : BDT n
  | node : Var n -> BDT n -> BDT n -> BDT n.

Definition Dimension (n : nat) (bdt : BDT n) : nat :=
  match bdt return nat with
  | zero =>
      (* zero  *)  0
      (* one   *)
  | one => 0
      (* (node i bl bh) *)
  | node xi bl bh => Order n xi
  end.

Inductive dimension (n : nat) : BDT n -> nat -> Prop :=
  | dim_zero : dimension n (zero n) 0
  | dim_one : dimension n (one n) 0
  | dim_node :
      forall (xi : Var n) (bl bh : BDT n),
      dimension n (node n xi bl bh) (Order n xi).
Hint Resolve dim_zero dim_one dim_node.

Lemma dim_functional :
 forall (n d : nat) (bdt : BDT n), dimension n bdt d -> d = Dimension n bdt.
Proof.
simple induction 1; simpl in |- *; auto with arith bdd.
Qed.
Hint Resolve dim_functional.

Inductive node_decomposition (n : nat) (bdt : BDT n) (d : nat) : Prop :=
    node_exist :
      forall (x : Var n) (bl bh : BDT n),
      Order n x = d -> node n x bl bh = bdt -> node_decomposition n bdt d.

Let dim_inv (n : nat) (bdt : BDT n) (d : nat) : Prop :=
  match d return Prop with
  | O =>
      (* O *)  zero n = bdt \/ one n = bdt
      (* S k *)
  | S k => node_decomposition n bdt d
  end.

Lemma p_dim_inv :
 forall (n d : nat) (bdt : BDT n), dimension n bdt d -> dim_inv n bdt d.
Proof.
simple induction 1; simpl in |- *; auto with arith bdd.
intros.
elim (Order_S n xi).
intros x E; rewrite E; simpl in |- *.
apply node_exist with xi bl bh; auto with arith bdd.
Qed.
Hint Resolve p_dim_inv.

Lemma dim_Dim :
 forall (n : nat) (bdt : BDT n), dimension n bdt (Dimension n bdt).
Proof.
intro n.
simple induction bdt; simpl in |- *; auto with arith bdd.
Qed.
Hint Resolve dim_Dim.

Lemma Exist_dim :
 forall (n : nat) (bdt : BDT n), exists d : nat, dimension n bdt d.
Proof.
intros n bdt.
exists (Dimension n bdt); auto with arith bdd.
Qed.

Lemma Dim_le_n : forall (n d : nat) (bdt : BDT n), Dimension n bdt <= n.
Proof.
simple induction bdt; simpl in |- *; auto with arith bdd.
Qed.
Hint Resolve Dim_le_n.

Inductive BDT_eq (n : nat) : BDT n -> BDT n -> Prop :=
  | BDT_eq_0 : BDT_eq n (zero n) (zero n)
  | BDT_eq_1 : BDT_eq n (one n) (one n)
  | BDT_eq_node :
      forall (bl1 bl2 bh1 bh2 : BDT n) (xi1 xi2 : Var n),
      BDT_eq n bl1 bl2 ->
      BDT_eq n bh1 bh2 ->
      eq_Var n xi1 xi2 -> BDT_eq n (node n xi1 bl1 bh1) (node n xi2 bl2 bh2).
Hint Resolve BDT_eq_0 BDT_eq_1 BDT_eq_node.

Definition inv_BDT_eq (n : nat) (bdt1 : BDT n) : BDT n -> Prop :=
  match bdt1 return (BDT n -> Prop) with
  | zero =>
      (* zero *)
      fun bdt2 : BDT n =>
      match bdt2 return Prop with
      | zero =>
          (* zero *)  True
          (* one  *)
      | one => False
          (* node *)
      | node x2 b2l b2h => False
      end
      (* one  *)
  | one =>
      fun bdt2 : BDT n =>
      match bdt2 return Prop with
      | zero =>
          (* zero *)  False
          (* one  *)
      | one => True
          (* node *)
      | node x2 b2l b2h => False
      end
      (* node *)
  | node x1 b1l b1h =>
      fun bdt2 : BDT n =>
      match bdt2 return Prop with
      | zero =>
          (* zero *)  False
          (* one  *)
      | one => False
          (* node *)
      | node x2 b2l b2h =>
          (BDT_eq n b1l b2l /\ BDT_eq n b1h b2h) /\ eq_Var n x1 x2
      end
  end.

Lemma p_inv_BDT_eq :
 forall (n : nat) (bdt1 bdt2 : BDT n),
 BDT_eq n bdt1 bdt2 -> inv_BDT_eq n bdt1 bdt2.
Proof.
simple induction 1; simpl in |- *; auto with arith bdd.
Qed.
Hint Resolve p_inv_BDT_eq.

Lemma ne_zero_one : forall n : nat, ~ BDT_eq n (zero n) (one n).
Proof.
unfold not in |- *.
intros n H_absurde.
change (inv_BDT_eq n (zero n) (one n)) in |- *; auto with arith bdd.
Qed.
Hint Resolve ne_zero_one.

Lemma ne_zero_node :
 forall (n : nat) (x2 : Var n) (b2l b2h : BDT n),
 ~ BDT_eq n (zero n) (node n x2 b2l b2h).
Proof.
unfold not in |- *.
intros n x2 b2l b2h H_absurde.
change (inv_BDT_eq n (zero n) (node n x2 b2l b2h)) in |- *;
 auto with arith bdd.
Qed.
Hint Resolve ne_zero_node.

Lemma ne_one_zero : forall n : nat, ~ BDT_eq n (one n) (zero n).
Proof.
unfold not in |- *.
intros n H_absurde.
change (inv_BDT_eq n (one n) (zero n)) in |- *; auto with arith bdd.
Qed.
Hint Resolve ne_one_zero.

Lemma ne_one_node :
 forall (n : nat) (x2 : Var n) (b2l b2h : BDT n),
 ~ BDT_eq n (one n) (node n x2 b2l b2h).
Proof.
unfold not in |- *.
intros n x2 b2l b2h H_absurde.
change (inv_BDT_eq n (one n) (node n x2 b2l b2h)) in |- *;
 auto with arith bdd.
Qed.
Hint Resolve ne_one_node.

Lemma inv_BDT_eq_node :
 forall (n : nat) (x1 x2 : Var n) (b1l b1h b2l b2h : BDT n),
 BDT_eq n (node n x1 b1l b1h) (node n x2 b2l b2h) ->
 (BDT_eq n b1l b2l /\ BDT_eq n b1h b2h) /\ eq_Var n x1 x2.
Proof.
intros n x1 x2 b1l b1h b2l b2h node1_eq_node2.
change (inv_BDT_eq n (node n x1 b1l b1h) (node n x2 b2l b2h)) in |- *;
 auto with arith bdd.
Qed.

Lemma ne_node_zero :
 forall (n : nat) (x1 : Var n) (b1l b1h : BDT n),
 ~ BDT_eq n (node n x1 b1l b1h) (zero n).
Proof.
unfold not in |- *.
intros n x1 b1l b1h H_absurde.
change (inv_BDT_eq n (node n x1 b1l b1h) (zero n)) in |- *;
 auto with arith bdd.
Qed.
Hint Resolve ne_node_zero.

Lemma ne_node_one :
 forall (n : nat) (x1 : Var n) (b1l b1h : BDT n),
 ~ BDT_eq n (node n x1 b1l b1h) (one n).
Proof.
unfold not in |- *.
intros n x1 b1l b1h H_absurde.
change (inv_BDT_eq n (node n x1 b1l b1h) (one n)) in |- *;
 auto with arith bdd.
Qed.
Hint Resolve ne_node_one.

Inductive OBDT (n : nat) : BDT n -> Prop :=
  | order_0 : OBDT n (zero n)
  | order_1 : OBDT n (one n)
  | order_node :
      forall (xi : Var n) (bl bh : BDT n),
      OBDT n bl ->
      OBDT n bh ->
      Order n xi > Dimension n bl ->
      Order n xi > Dimension n bh ->
      ~ BDT_eq n bl bh -> OBDT n (node n xi bl bh).

Hint Resolve order_0 order_1 order_node.

Definition inv_OBDT_Order (n : nat) (bdt : BDT n) : Prop :=
  match bdt return Prop with
  | zero =>
      (* zero *)  True
      (* one  *)
  | one => True
      (* node xi bl bh *)
  | node xi bl bh =>
      Order n xi > Dimension n bl /\ Order n xi > Dimension n bh
  end.

Lemma p_inv_OBDT_order :
 forall (n : nat) (bdt : BDT n), OBDT n bdt -> inv_OBDT_Order n bdt.
Proof.
simple induction 1; simpl in |- *; auto with arith bdd.
Qed.
Hint Resolve p_inv_OBDT_order.

Definition inv_OBDT_eq (n : nat) (bdt : BDT n) : Prop :=
  match bdt return Prop with
  | zero =>
      (* zero *)  True
      (* one  *)
  | one => True
      (* node xi bl bh *)
  | node xi bl bh => ~ BDT_eq n bl bh
  end.

Lemma p_inv_OBDT_eq :
 forall (n : nat) (bdt : BDT n), OBDT n bdt -> inv_OBDT_eq n bdt.
Proof.
simple induction 1; simpl in |- *; auto with arith bdd.
Qed.
Hint Resolve p_inv_OBDT_eq.

Definition inv_OBDT_bl (n : nat) (bdt : BDT n) : Prop :=
  match bdt return Prop with
  | zero =>
      (* zero *)  True
      (* one  *)
  | one => True
      (* node xi bl bh *)
  | node xi bl bh => OBDT n bl
  end.

Lemma p_inv_OBDT_bl :
 forall (n : nat) (bdt : BDT n), OBDT n bdt -> inv_OBDT_bl n bdt.
Proof.
simple induction 1; simpl in |- *; auto with arith bdd.
Qed.
Hint Resolve p_inv_OBDT_bl.

Definition inv_OBDT_bh (n : nat) (bdt : BDT n) : Prop :=
  match bdt return Prop with
  | zero =>
      (* zero *)  True
      (* one  *)
  | one => True
      (* node xi bl bh *)
  | node xi bl bh => OBDT n bh
  end.

Lemma p_inv_OBDT_bh :
 forall (n : nat) (bdt : BDT n), OBDT n bdt -> inv_OBDT_bh n bdt.
Proof.
simple induction 1; simpl in |- *; auto with arith bdd.
Qed.
Hint Resolve p_inv_OBDT_bh.

Lemma Dim_node_Dim_bh :
 forall (n : nat) (bl bh : BDT n) (xi : Var n),
 OBDT n (node n xi bl bh) ->
 forall dn dh : nat,
 dimension n (node n xi bl bh) dn -> dimension n bh dh -> dn > dh.
Proof.
intros n bl bh xi H_OBDT dn dh Def_dn Def_dh.
replace dn with (Dimension n (node n xi bl bh)); try symmetry  in |- *;
 auto with arith bdd.
replace dh with (Dimension n bh); try symmetry  in |- *; auto with arith bdd.
simpl in |- *.
cut (inv_OBDT_Order n (node n xi bl bh)); auto with arith bdd.
simpl in |- *; simple induction 1; auto with arith bdd.
Qed.

Lemma Dim_node_Dim_bl :
 forall (n : nat) (bl bh : BDT n) (xi : Var n),
 OBDT n (node n xi bl bh) ->
 forall dn dl : nat,
 dimension n (node n xi bl bh) dn -> dimension n bl dl -> dn > dl.
Proof.
intros n bl bh xi H_OBDT dn dl Def_dn Def_dl.
replace dn with (Dimension n (node n xi bl bh)); try symmetry  in |- *;
 auto with arith bdd.
replace dl with (Dimension n bl); try symmetry  in |- *; auto with arith bdd.
simpl in |- *.
cut (inv_OBDT_Order n (node n xi bl bh)); auto with arith bdd.
simpl in |- *; simple induction 1; auto with arith bdd.
Qed.

(********************         From BDT to BF             *******************)

Definition Fun (n : nat) (bdt : BDT n) : BF n :=
  (fix F (b : BDT n) : BF n :=
     match b with
     | zero => fun _ : Assign n => false
     | one => fun _ : Assign n => true
     | node v b0 b1 => fun A : Assign n => if A v then F b1 A else F b0 A
     end) bdt.
(* zero  *)
(* one   *)
(* node xi bl bh *)
(* true *)
(* false *)

Lemma ne_Fzero_Fone :
 forall n : nat, ~ BF_eq n (Fun n (zero n)) (Fun n (one n)).
Proof.
intro n.
simpl in |- *.
unfold not, BF_eq in |- *.
intro H_absurd.
absurd (false = true); auto with bool.
apply H_absurd; exact (fun x : Var n => true).
Qed.
Hint Resolve ne_Fzero_Fone.

Lemma ne_Fone_Fzero :
 forall n : nat, ~ BF_eq n (Fun n (one n)) (Fun n (zero n)).
Proof.
intro n.
unfold not in |- *; intro H1.
cut (~ BF_eq n (Fun n (zero n)) (Fun n (one n))); auto with arith bdd.
Qed.
Hint Resolve ne_Fone_Fzero.

Lemma Restr_node_Restr_low :
 forall (n : nat) (x : Var n) (bl bh : BDT n),
 BF_eq n (Restr n (Fun n (node n x bl bh)) x false)
   (Restr n (Fun n bl) x false).
Proof.
intros n x bl bh.
unfold BF_eq in |- *.
intro A.
unfold Restr at 1 in |- *; simpl in |- *.
unfold Upd at 1 in |- *; simpl in |- *.
elim (eq_Var_dec n x x).
intro x_eq_x.
change (Restr n (Fun n bl) x false A = Restr n (Fun n bl) x false A) in |- *;
 auto with arith bdd.
intro H_absurde.
absurd (eq_Var n x x); auto with arith bdd.
Qed.
Hint Resolve Restr_node_Restr_low.

Lemma Restr_node_Restr_high :
 forall (n : nat) (x : Var n) (bl bh : BDT n),
 BF_eq n (Restr n (Fun n (node n x bl bh)) x true)
   (Restr n (Fun n bh) x true).
Proof.
intros n x bl bh.
unfold BF_eq in |- *.
intro A.
unfold Restr at 1 in |- *; simpl in |- *.
unfold Upd at 1 in |- *; simpl in |- *.
elim (eq_Var_dec n x x).
intro x_eq_x.
change (Restr n (Fun n bh) x true A = Restr n (Fun n bh) x true A) in |- *;
 auto with arith bdd.
intro H_absurde.
absurd (eq_Var n x x); auto with arith bdd.
Qed.
Hint Resolve Restr_node_Restr_high.

(*---------------------------------------------------------------------------*)
Lemma vars_sup_dim_non_dep :
 forall (n : nat) (bdt : BDT n),
 OBDT n bdt ->
 forall x : Var n,
 Order n x > Dimension n bdt ->
 forall b : bool, BF_eq n (Restr n (Fun n bdt) x b) (Fun n bdt).
(*---------------------------------------------------------------------------*)
Proof.
cut
 (forall (n k : nat) (bdt : BDT n),
  OBDT n bdt ->
  Dimension n bdt <= k ->
  forall x : Var n,
  Order n x > Dimension n bdt ->
  forall b : bool, BF_eq n (Restr n (Fun n bdt) x b) (Fun n bdt)).
intros Coupure n bdt bdt_OBDT x x_gt_Dim_bdt b.
apply Coupure with (k := n); auto with arith bdd.
simple induction k.
       (* k = O *)
intros bdt bdt_OBDT Dim_O x gt_Orderx_Dim b.
cut (dim_inv n bdt 0).
unfold dim_inv in |- *.
do 2 simple induction 1; simpl in |- *; unfold BF_eq in |- *;
 auto with arith bdd.
apply p_dim_inv.
elimtype (Dimension n bdt = 0); try apply sym_equal; auto with arith bdd.
     (* k -> (S k) *)
intros l Hl bdt H_OBDT H_dim x H_order_x b.
elim (le_nSm_le_nm_or_eq l (Dimension n bdt)); try assumption;
 intro H_dim_bdt; auto with arith bool bdd.
cut (node_decomposition n bdt (S l)).
simple induction 1.
intros xi bl bh Order_xi decomp_bdt.
unfold BF_eq in |- *.
intro A.
elim decomp_bdt; simpl in |- *.
unfold Restr in |- *; simpl in |- *.
elimtype (A xi = Upd n A x b xi).
elim (A xi).
(*---- (Fun n bh (Upd n A x b))=(Fun n bh A) ---*)
change (Restr n (Fun n bh) x b A = Fun n bh A) in |- *.
cut (forall A : Assign n, Restr n (Fun n bh) x b A = Fun n bh A);
 auto with arith bool bdd.
change (BF_eq n (Restr n (Fun n bh) x b) (Fun n bh)) in |- *.
apply Hl.
change (inv_OBDT_bh n (node n xi bl bh)) in |- *; rewrite decomp_bdt;
 auto with arith bool bdd.
apply gt_S_le.
replace (S l) with (Dimension n bdt).
apply Dim_node_Dim_bh with n bl bh xi; try rewrite decomp_bdt;
 auto with arith bool bdd.
apply gt_trans with (m := Dimension n bdt); auto with arith bool bdd.
apply Dim_node_Dim_bh with n bl bh xi; try rewrite decomp_bdt;
 auto with arith bool bdd.
(*---- (Fun n bl (Upd n A x b))=(Fun n bl A) ----*)
change (Restr n (Fun n bl) x b A = Fun n bl A) in |- *.
cut (forall A : Assign n, Restr n (Fun n bl) x b A = Fun n bl A);
 auto with arith bool bdd.
change (BF_eq n (Restr n (Fun n bl) x b) (Fun n bl)) in |- *.
apply Hl.
change (inv_OBDT_bl n (node n xi bl bh)) in |- *; rewrite decomp_bdt;
 auto with arith bool bdd.
apply gt_S_le.
replace (S l) with (Dimension n bdt).
apply Dim_node_Dim_bl with n bl bh xi; try rewrite decomp_bdt;
 auto with arith bool bdd.
apply gt_trans with (m := Dimension n bdt); auto with arith bool bdd.
apply Dim_node_Dim_bl with n bl bh xi; try rewrite decomp_bdt;
 auto with arith bool bdd.
(*---- (A xi)=(Upd n A x b xi) -----*)
symmetry  in |- *; apply Upd_xi_xj.
unfold eq_Var, not in |- *; intro E.
generalize H_order_x; rewrite H_dim_bdt; elim E; rewrite Order_xi.
intro; apply (gt_irrefl (S l)); trivial.
(*---- (node_decomposition n bdt (S l)) -----*)
change (dim_inv n bdt (S l)) in |- *.
rewrite <- H_dim_bdt; auto with arith bool bdd.
Qed.

Lemma vars_sup_dim_non_dep2 :
 forall (n : nat) (bdt : BDT n),
 OBDT n bdt ->
 forall x : Var n, Order n x > Dimension n bdt -> ~ Dep_Var n (Fun n bdt) x.
Proof.
intros n bdt On x H_Order_x.
unfold not in |- *.
intro H_absurde.
cut (~ BF_eq n (Restr n (Fun n bdt) x true) (Restr n (Fun n bdt) x false));
 auto with arith bool bdd.
unfold not in |- *.
intro H; apply H.
apply BF_eq_trans with (f2 := Fun n bdt).
apply vars_sup_dim_non_dep; auto with arith bool bdd.
apply BF_eq_sym; apply vars_sup_dim_non_dep; auto with arith bool bdd.
Qed.

(*--------------------------------------------------------------------------*)
  Lemma BDT_iso_BDF_eq :
   forall (n : nat) (bdt1 bdt2 : BDT n),
   BDT_eq n bdt1 bdt2 -> BF_eq n (Fun n bdt1) (Fun n bdt2).
(*--------------------------------------------------------------------------*)
Proof.
simple induction 1; auto with arith bool bdd.
intros bl1 bl2 bh1 bh2 xi1 xi2 bl1_iso_bl2 Fbl1_eq_Fbl2 bh1_iso_bh2
 Fbh1_eq_Fbh2 xi1_eq_xi2.
unfold BF_eq in |- *; intro A; simpl in |- *.
elimtype (A xi1 = A xi2).
unfold BF_eq in Fbh1_eq_Fbh2.
unfold BF_eq in Fbl1_eq_Fbl2.
elim (A xi1); auto with arith bool bdd.
pattern xi2 in |- *; apply Proof_irrelevance with n xi1;
 auto with arith bool bdd.
Qed.
Hint Resolve BDT_iso_BDF_eq.

(*--------------------------------------------------------------------------*)
  Lemma Fun_eq_OBDT_eq :
   forall (n : nat) (bdt1 bdt2 : BDT n),
   OBDT n bdt1 ->
   OBDT n bdt2 -> BF_eq n (Fun n bdt1) (Fun n bdt2) -> BDT_eq n bdt1 bdt2.
(*--------------------------------------------------------------------------*)
Proof.
intros n bdt1 bdt2 H H0 H1.
cut
 (forall (n k : nat) (bdt1 bdt2 : BDT n),
  Dimension n bdt1 <= k ->
  Dimension n bdt2 <= k ->
  OBDT n bdt1 ->
  OBDT n bdt2 -> BF_eq n (Fun n bdt1) (Fun n bdt2) -> BDT_eq n bdt1 bdt2).
intro Fun_eq_OBDT_eq_dimk.
apply Fun_eq_OBDT_eq_dimk with (k := n); auto with arith bool bdd.
(* Cut *)
clear H1 H0 H bdt2 bdt1 n.
intro n.
simple induction k.
(*------ k= O ------*)
intros bdt1 bdt2 H_dim1 H_dim2 H_OBDT1 H_OBDT2.
cut (dim_inv n bdt1 0).
cut (dim_inv n bdt2 0).
unfold dim_inv in |- *.
do 4 simple induction 1; auto with arith bool bdd.
intro Fone_eq_Fzero.
unfold BF_eq, Fun in Fone_eq_Fzero.
absurd (true = false); auto with arith bool bdd.
apply Fone_eq_Fzero; exact (fun x : Var n => true).
intro Fzero_eq_Fone.
unfold BF_eq, Fun in Fzero_eq_Fone.
absurd (false = true); auto with arith bool bdd.
apply Fzero_eq_Fone; exact (fun x : Var n => true).
(* (dim_inv n bdt2 O) *)
cut (0 = Dimension n bdt2); try apply le_n_O_eq; try assumption.
intro Dim_bdt2.
apply p_dim_inv; rewrite Dim_bdt2; auto with arith bool bdd.
(* (dim_inv n bdt1 O) *)
cut (0 = Dimension n bdt1); try apply le_n_O_eq; try assumption.
intro Dim_bdt1.
apply p_dim_inv; rewrite Dim_bdt1; auto with arith bool bdd.
(*------  k -> (S k) -------*)
intros l Hl.
intros bdt1 bdt2 Dim_bdt1 Dim_bdt2 OBDT1 OBDT2 Fun1_eq_Fun2.
elim (le_nSm_le_nm_or_eq l (Dimension n bdt1)); try assumption;
 elim (le_nSm_le_nm_or_eq l (Dimension n bdt2)); try assumption;
 auto with arith bool bdd.
(*--- Case Dim(bdt1)<=l Dim(bdt2)=(S l) ---*)
intros Dim2_eq_Sl Dim1_le_l.
cut (node_decomposition n bdt2 (S l)).
simple induction 1.
intros x b2l b2h Order_x decomp_bdt2.
absurd (BDT_eq n b2l b2h).
    (* ~(BDT_eq n b2l b2h) *)
change (inv_OBDT_eq n (node n x b2l b2h)) in |- *.
replace (node n x b2l b2h) with bdt2; auto with arith bool bdd.
    (* (BDT_eq n b2l b2h) *)
cut (OBDT n bdt2); try assumption.
rewrite <- decomp_bdt2.
intro OBDT_node_b2.
cut (OBDT n b2l).
intro OBDT_b2l.
cut (OBDT n b2h).
intro OBDT_b2h.
apply Hl; auto with arith bool bdd.
      (* (le (Dimension n b2l) l) *)
apply gt_S_le.
replace (S l) with (Dimension n bdt2).
apply Dim_node_Dim_bl with n b2l b2h x; auto with arith bool bdd.
rewrite decomp_bdt2; auto with arith bool bdd.
      (* (le (Dimension n b2h) l) *)
apply gt_S_le.
replace (S l) with (Dimension n bdt2).
apply Dim_node_Dim_bh with n b2l b2h x; auto with arith bool bdd.
rewrite decomp_bdt2; auto with arith bool bdd.
      (* (BF_eq n (Fun n b2l) (Fun n b2h)) *)
apply BF_eq_trans with (Fun n bdt1).
apply BF_eq_trans with (Restr n (Fun n bdt1) x false).
apply BF_eq_trans with (Restr n (Fun n bdt2) x false);
 auto with arith bool bdd.
apply BF_eq_trans with (Restr n (Fun n (node n x b2l b2h)) x false).
  (* (BF_eq n (Fun n b2l) (Restr n (Fun n (node n x b2l b2h)) x false)) *)
apply BF_eq_trans with (Restr n (Fun n b2l) x false);
 auto with arith bool bdd.
(* Use: Restr_node_Restr_low *)
apply BF_eq_sym.
apply vars_sup_dim_non_dep; auto with arith bool bdd.
  (* (gt (Order n x) (Dimension n b2l)) *)
rewrite Order_x.
rewrite <- Dim2_eq_Sl.
rewrite <- decomp_bdt2.
apply Dim_node_Dim_bl with (n := n) (bl := b2l) (bh := b2h) (xi := x);
 auto with arith bool bdd.
rewrite decomp_bdt2; auto with arith bool bdd.
  (*  (BF_eq n (Restr n (Fun n bdt1) x false) (Fun n bdt1)) *)
apply vars_sup_dim_non_dep; auto with arith bool bdd.
rewrite Order_x.
apply gt_le_trans with (n := S l) (m := l) (p := Dimension n bdt1);
 auto with arith bool bdd.
  (*  (BF_eq n (Fun n bdt1) (Fun n b2h)) *)
apply BF_eq_trans with (Restr n (Fun n bdt1) x true).
apply BF_eq_sym; apply vars_sup_dim_non_dep; auto with arith bool bdd.
rewrite Order_x.
apply gt_le_trans with (n := S l) (m := l) (p := Dimension n bdt1);
 auto with arith bool bdd.
  (* (BF_eq n (Restr n (Fun n bdt1) x true) (Fun n b2h)) *)
apply BF_eq_trans with (Restr n (Fun n bdt2) x true);
 auto with arith bool bdd.
apply BF_eq_trans with (Restr n (Fun n (node n x b2l b2h)) x true).
rewrite decomp_bdt2; auto with arith bool bdd.
  (*  (BF_eq n (Restr n (Fun n (node n x b2l b2h)) x true) (Fun n b2h)) *)
apply BF_eq_trans with (Restr n (Fun n b2h) x true); auto with arith bool bdd.
(* Use: Restr_node_Restr_high *)
apply vars_sup_dim_non_dep; auto with arith bool bdd.
  (* (gt (Order n x) (Dimension n b2h)) *)
rewrite Order_x.
rewrite <- Dim2_eq_Sl.
rewrite <- decomp_bdt2.
apply Dim_node_Dim_bh with (n := n) (bl := b2l) (bh := b2h) (xi := x);
 auto with arith bool bdd.
      (* (OBDT n b2h) *)
change (inv_OBDT_bh n (node n x b2l b2h)) in |- *; auto with arith bool bdd.
      (* (OBDT n b2l) *)
change (inv_OBDT_bl n (node n x b2l b2h)) in |- *; auto with arith bool bdd.
    (* (node_decomposition n bdt2 (S l)) *)
change (dim_inv n bdt2 (S l)) in |- *; rewrite <- Dim2_eq_Sl;
 auto with arith bool bdd.
(*--- Case Dim(bdt1)=Sl Dim(bdt2)<=l ---*)
intros Dim2_le_l Dim1_eq_Sl.
cut (node_decomposition n bdt1 (S l)).
simple induction 1.
intros x b1l b1h Order_x decomp_bdt1.
absurd (BDT_eq n b1l b1h).
    (* ~(BDT_eq n b1l b1h) *)
change (inv_OBDT_eq n (node n x b1l b1h)) in |- *.
replace (node n x b1l b1h) with bdt1; auto with arith bool bdd.
    (* (BDT_eq n b1l b1h) *)
cut (OBDT n bdt1); try assumption.
rewrite <- decomp_bdt1.
intro OBDT_node_b1.
cut (OBDT n b1l).
intro OBDT_b1l.
cut (OBDT n b1h).
intro OBDT_b1h.
apply Hl; auto with arith bool bdd.
      (* (le (Dimension n b1l) l) *)
apply gt_S_le.
replace (S l) with (Dimension n bdt1).
apply Dim_node_Dim_bl with n b1l b1h x; auto with arith bool bdd.
rewrite decomp_bdt1; auto with arith bool bdd.
      (* (le (Dimension n b1h) l) *)
apply gt_S_le.
replace (S l) with (Dimension n bdt1).
apply Dim_node_Dim_bh with n b1l b1h x; auto with arith bool bdd.
rewrite decomp_bdt1; auto with arith bool bdd.
      (* (BF_eq n (Fun n b1l) (Fun n b1h)) *)
apply BF_eq_trans with (Fun n bdt2).
apply BF_eq_trans with (Restr n (Fun n bdt2) x false).
apply BF_eq_trans with (Restr n (Fun n bdt1) x false);
 auto with arith bool bdd.
apply BF_eq_trans with (Restr n (Fun n (node n x b1l b1h)) x false).
  (* (BF_eq n (Fun n b1l) (Restr n (Fun n (node n x b1l b1h)) x false)) *)
apply BF_eq_trans with (Restr n (Fun n b1l) x false);
 auto with arith bool bdd.
(* Use: Restr_node_Restr_low *)
apply BF_eq_sym.
apply vars_sup_dim_non_dep; auto with arith bool bdd.
  (* (gt (Order n x) (Dimension n b1l)) *)
rewrite Order_x.
rewrite <- Dim1_eq_Sl.
rewrite <- decomp_bdt1.
apply Dim_node_Dim_bl with (n := n) (bl := b1l) (bh := b1h) (xi := x);
 auto with arith bool bdd.
rewrite decomp_bdt1; auto with arith bool bdd.
  (* (BF_eq n (Restr n (Fun n bdt2) x false) (Fun n bdt2)) *)
apply vars_sup_dim_non_dep; auto with arith bool bdd.
rewrite Order_x.
apply gt_le_trans with (n := S l) (m := l) (p := Dimension n bdt2);
 auto with arith bool bdd.
  (* (BF_eq n (Fun n bdt2) (Fun n b1h)) *)
apply BF_eq_trans with (Restr n (Fun n bdt2) x true).
apply BF_eq_sym; apply vars_sup_dim_non_dep; auto with arith bool bdd.
rewrite Order_x.
apply gt_le_trans with (n := S l) (m := l) (p := Dimension n bdt2);
 auto with arith bool bdd.
  (* (BF_eq n (Restr n (Fun n bdt2) x true) (Fun n b1h)) *)
apply BF_eq_trans with (Restr n (Fun n bdt1) x true);
 auto with arith bool bdd.
apply BF_eq_trans with (Restr n (Fun n (node n x b1l b1h)) x true).
rewrite decomp_bdt1; auto with arith bool bdd.
  (*  (BF_eq n (Restr n (Fun n (node n x b1l b1h)) x true) (Fun n b1h)) *)
apply BF_eq_trans with (Restr n (Fun n b1h) x true); auto with arith bool bdd.
(* Use: Restr_node_Restr_high *)
apply vars_sup_dim_non_dep; auto with arith bool bdd.
  (* (gt (Order n x) (Dimension n b1h)) *)
rewrite Order_x.
rewrite <- Dim1_eq_Sl.
rewrite <- decomp_bdt1.
apply Dim_node_Dim_bh with (n := n) (bl := b1l) (bh := b1h) (xi := x);
 auto with arith bool bdd.
      (* (OBDT n b1h) *)
change (inv_OBDT_bh n (node n x b1l b1h)) in |- *; auto with arith bool bdd.
      (* (OBDT n b1l) *)
change (inv_OBDT_bl n (node n x b1l b1h)) in |- *; auto with arith bool bdd.
    (* (node_decomposition n bdt1 (S l)) *)
change (dim_inv n bdt1 (S l)) in |- *; rewrite <- Dim1_eq_Sl;
 auto with arith bool bdd.
(*-----    Case Dim(bdt1)=Sl Dim(bdt2)=Sl    ------*)
intros Dim2_eq_Sl Dim1_eq_Sl.
cut (node_decomposition n bdt1 (S l)).
simple induction 1.
intros x1 b1l b1h Order_x1 decomp_bdt1.
cut (node_decomposition n bdt2 (S l)).
simple induction 1.
intros x2 b2l b2h Order_x2 decomp_bdt2.
cut (OBDT n bdt1); try assumption.
rewrite <- decomp_bdt1.
intro OBDT_node_b1.
cut (OBDT n bdt2); try assumption.
rewrite <- decomp_bdt2.
intro OBDT_node_b2.
cut (eq_Var n x1 x2).
intro x1_eq_x2.
apply BDT_eq_node; auto with arith bool bdd.
   (* (BDT_eq n b1l b2l) *)
cut (OBDT n b1l).
intro OBDT_b1l.
cut (OBDT n b2l).
intro OBDT_b2l.
apply Hl; auto with arith bool bdd.
       (* (le (Dimension n b1l) l) *)
apply gt_S_le.
replace (S l) with (Dimension n bdt1).
apply Dim_node_Dim_bl with n b1l b1h x1; auto with arith bool bdd.
rewrite decomp_bdt1; auto with arith bool bdd.
       (* (le (Dimension n b2l) l) *)
apply gt_S_le.
replace (S l) with (Dimension n bdt2).
apply Dim_node_Dim_bl with n b2l b2h x2; auto with arith bool bdd.
rewrite decomp_bdt2; auto with arith bool bdd.
       (* (BF_eq n (Fun n b1l) (Fun n b2l)) *)
apply BF_eq_trans with (Restr n (Fun n (node n x1 b1l b1h)) x1 false).
apply BF_eq_sym.
apply BF_eq_trans with (Restr n (Fun n b1l) x1 false);
 auto with arith bool bdd.
apply vars_sup_dim_non_dep; auto with arith bool bdd.
  (* (gt (Order n x1) (Dimension n b1l)) *)
rewrite Order_x1.
rewrite <- Dim1_eq_Sl.
rewrite <- decomp_bdt1.
apply Dim_node_Dim_bl with (n := n) (bl := b1l) (bh := b1h) (xi := x1);
 auto with arith bool bdd.
  (*  (BF_eq n (Restr n (Fun n (node n x1 b1l b1h)) x1 false) (Fun n b2l)) *)
apply BF_eq_trans with (Restr n (Fun n (node n x2 b2l b2h)) x2 false).
rewrite decomp_bdt1; rewrite decomp_bdt2.
pattern x2 in |- *.
apply Proof_irrelevance with (n := n) (x := x1); auto with arith bool bdd.
apply BF_eq_trans with (Restr n (Fun n b2l) x2 false);
 auto with arith bool bdd.
apply vars_sup_dim_non_dep; auto with arith bool bdd.
  (* (gt (Order n x2) (Dimension n b2l)) *)
rewrite Order_x2.
rewrite <- Dim2_eq_Sl.
rewrite <- decomp_bdt2.
apply Dim_node_Dim_bl with (n := n) (bl := b2l) (bh := b2h) (xi := x2);
 auto with arith bool bdd.
       (*  (OBDT n b2l) *)
change (inv_OBDT_bl n (node n x2 b2l b2h)) in |- *; auto with arith bool bdd.
       (*  (OBDT n b1l) *)
change (inv_OBDT_bl n (node n x1 b1l b1h)) in |- *; auto with arith bool bdd.
  (* (BDT_eq n b1h b2h) *)
cut (OBDT n b1h).
intro OBDT_b1h.
cut (OBDT n b2h).
intro OBDT_b2h.
apply Hl; auto with arith bool bdd.
       (* (le (Dimension n b1h) l) *)
apply gt_S_le.
replace (S l) with (Dimension n bdt1).
apply Dim_node_Dim_bh with n b1l b1h x1; auto with arith bool bdd.
rewrite decomp_bdt1; auto with arith bool bdd.
       (* (le (Dimension n b2h) l) *)
apply gt_S_le.
replace (S l) with (Dimension n bdt2).
apply Dim_node_Dim_bh with n b2l b2h x2; auto with arith bool bdd.
rewrite decomp_bdt2; auto with arith bool bdd.
       (* (BF_eq n (Fun n b1h) (Fun n b2h)) *)
apply BF_eq_trans with (Restr n (Fun n (node n x1 b1l b1h)) x1 true).
apply BF_eq_sym.
apply BF_eq_trans with (Restr n (Fun n b1h) x1 true);
 auto with arith bool bdd.
apply vars_sup_dim_non_dep; auto with arith bool bdd.
  (* (gt (Order n x1) (Dimension n b1h)) *)
rewrite Order_x1.
rewrite <- Dim1_eq_Sl.
rewrite <- decomp_bdt1.
apply Dim_node_Dim_bh with (n := n) (bl := b1l) (bh := b1h) (xi := x1);
 auto with arith bool bdd.
  (*  (BF_eq n (Restr n (Fun n (node n x1 b1l b1h)) x1 true) (Fun n b2h)) *)
apply BF_eq_trans with (Restr n (Fun n (node n x2 b2l b2h)) x2 true).
rewrite decomp_bdt1; rewrite decomp_bdt2.
pattern x2 in |- *.
apply Proof_irrelevance with (n := n) (x := x1); auto with arith bool bdd.
apply BF_eq_trans with (Restr n (Fun n b2h) x2 true);
 auto with arith bool bdd.
apply vars_sup_dim_non_dep; auto with arith bool bdd.
  (* (gt (Order n x2) (Dimension n b2h)) *)
rewrite Order_x2.
rewrite <- Dim2_eq_Sl.
rewrite <- decomp_bdt2.
apply Dim_node_Dim_bh with (n := n) (bl := b2l) (bh := b2h) (xi := x2);
 auto with arith bool bdd.
       (*  (OBDT n b2h) *)
change (inv_OBDT_bh n (node n x2 b2l b2h)) in |- *; auto with arith bool bdd.
       (*  (OBDT n b1h) *)
change (inv_OBDT_bh n (node n x1 b1l b1h)) in |- *; auto with arith bool bdd.
      (* (eq_Var n x1 x2) *)
apply same_order_eq_Var with (k := S l); auto with arith bool bdd.
    (* (node_decomposition n bdt2 (S l)) *)
change (dim_inv n bdt2 (S l)) in |- *; rewrite <- Dim2_eq_Sl;
 auto with arith bool bdd.
    (* (node_decomposition n bdt1 (S l)) *)
change (dim_inv n bdt1 (S l)) in |- *; rewrite <- Dim1_eq_Sl;
 auto with arith bool bdd.
Qed.

(*---------------------------------------------------------------------------*)
  Lemma Dim_is_Greatest_Dep_Var :
   forall (n : nat) (bdt : BDT n),
   OBDT n bdt ->
   Dimension n bdt > 0 ->
   exists x : Var n,
     Order n x = Dimension n bdt /\ Greatest_Dep_Var n (Fun n bdt) x.
(*---------------------------------------------------------------------------*)
Proof.
intros n bdt On Dim.
cut (node_decomposition n bdt (Dimension n bdt)).
simple induction 1.
intros x bl bh Order_x decomp_bdt.
exists x; split; auto with arith bool bdd.
apply Def_GreatestDV.
(*-----  (Dep_Var n (Fun n bdt) x)----- *)
unfold Dep_Var in |- *.
cut (~ BF_eq n (Fun n bl) (Fun n bh)).
intro H1.
unfold not in H1.
unfold not in |- *.
intro H_absurde.
apply H1.
    (* (BF_eq n (Fun n bl) (Fun n bh)) *)
apply BF_eq_trans with (n := n) (f2 := Restr n (Fun n bh) x true).
apply
 BF_eq_trans with (n := n) (f2 := Restr n (Fun n (node n x bl bh)) x true);
 auto with arith bool bdd.
apply
 BF_eq_trans with (n := n) (f2 := Restr n (Fun n (node n x bl bh)) x false);
 [ idtac | apply BF_eq_sym; rewrite decomp_bdt; auto ].
apply BF_eq_trans with (n := n) (f2 := Restr n (Fun n bl) x false);
 [ idtac | apply BF_eq_sym; auto ].
apply BF_eq_sym.
 (*  (BF_eq n (Restr n (Fun n bl) x false) (Fun n bl)) *)
apply vars_sup_dim_non_dep.
change (inv_OBDT_bl n (node n x bl bh)) in |- *.
rewrite decomp_bdt; auto with arith bool bdd.
rewrite Order_x.
apply Dim_node_Dim_bl with (n := n) (bl := bl) (bh := bh) (xi := x);
 try rewrite decomp_bdt; auto with arith bool bdd.
 (*  (BF_eq n (Restr n (Fun n bh) x true) (Fun n bh))  *)
apply vars_sup_dim_non_dep.
change (inv_OBDT_bh n (node n x bl bh)) in |- *.
rewrite decomp_bdt; auto with arith bool bdd.
rewrite Order_x.
apply Dim_node_Dim_bh with (n := n) (bl := bl) (bh := bh) (xi := x);
 try rewrite decomp_bdt; auto with arith bool bdd.
 (* ~(BF_eq n (Fun n bl) (Fun n bh)) *)
apply Contra with (Q := BDT_eq n bl bh).
intro Fbl_eq_Fbh; apply Fun_eq_OBDT_eq.
change (inv_OBDT_bl n (node n x bl bh)) in |- *; rewrite decomp_bdt;
 auto with arith bool bdd.
change (inv_OBDT_bh n (node n x bl bh)) in |- *; rewrite decomp_bdt;
 auto with arith bool bdd.
auto with arith bool bdd.
change (inv_OBDT_eq n (node n x bl bh)) in |- *; rewrite decomp_bdt;
 auto with arith bool bdd.
 (*----- (xj:(Var n))(Dep_Var n (Fun n bdt) xj)->(le_Var n xj x) ----- *)
intros xj xj_Dep.
elim (le_or_gt_Var n xj x); auto with arith bool bdd.
intro H_absurde.
absurd (Dep_Var n (Fun n bdt) xj); auto with arith bool bdd.
apply vars_sup_dim_non_dep2; auto with arith bool bdd.
elim Order_x.
change (gt_Var n xj x) in |- *; assumption.
 (*  (node_decomposition n bdt (Dimension n bdt)) *)
cut (dim_inv n bdt (Dimension n bdt)); auto with arith bool bdd.
generalize Dim; elim (Dimension n bdt); trivial.
intros; absurd (0 > 0); auto with arith bool bdd.
Qed.

(*****************    Denotation of a function by a BDT   ******************)

Definition Denote (n : nat) (f : BF n) (bdt : BDT n) :=
  OBDT n bdt /\ BF_eq n f (Fun n bdt).

Lemma Denote_inv_eq :
 forall (n : nat) (f : BF n) (bdt : BDT n),
 Denote n f bdt -> BF_eq n f (Fun n bdt).
Proof.
intros n f bdt.
unfold Denote in |- *.
simple induction 1; auto with arith bool bdd.
Qed.
Hint Resolve Denote_inv_eq.

Lemma Denote_inv_OBDT :
 forall (n : nat) (f : BF n) (bdt : BDT n), Denote n f bdt -> OBDT n bdt.
Proof.
intros n f bdt.
unfold Denote in |- *.
simple induction 1; auto with arith bool bdd.
Qed.

author: coq-contribs

repo: canon-bdds


text:
(** * Interpretation of a hypersequent as a term in NNF *)
Require Import Rpos.
Require Import RL.hr.term.
Require Import RL.hr.hseq.
Require Import RL.hr.semantic.

Require Import List.
Require Import Lra.

Require Import RL.OLlibs.Permutation_Type_more.

Local Open Scope R_scope.

(** ** Interpretation of a sequent *)
Fixpoint sem_seq (T1 : sequent) :=
  match T1 with
  | nil => HR_zero
  | ((r , A) :: T1) => (r *S A) +S (sem_seq T1)
  end.

(** *** Properties of this interpretation *)
Lemma sem_seq_plus : forall T1 T2, sem_seq (T1 ++ T2) === sem_seq T1 +S sem_seq T2.
Proof.
  induction T1; intros T2.
  - rewrite commu_plus; now rewrite neutral_plus.
  - specialize (IHT1 T2).
    destruct a as (r , A).
    simpl; rewrite IHT1.
    now auto with MGA_solver.
Qed.

Lemma sem_seq_mul : forall T r, sem_seq (seq_mul r T) === r *S sem_seq T.
Proof.
  induction T; intros r.
  - now rewrite mul_0.
  - destruct a as [a Ha]; simpl.
    rewrite IHT.
    rewrite <-mul_assoc.
    auto with MGA_solver.
Qed.

(** In NNF, we can not multiply by 0 so the following lemma (stating that [\vec{r}.A] = \sum\vec{r}.[A]) require the vector to be non empty *)
Lemma sem_seq_vec : forall r A (Hnnil : r <> nil), sem_seq (vec r A) === (existT _ (sum_vec r) (sum_vec_non_nil _ Hnnil)) *S A.
Proof.
  induction r; intros A Hnnil.
  { exfalso; auto. }
  destruct r as [ | b r].
  - simpl in *.
    replace (existT (fun r : R => (0 <? r) = true) (projT1 a + 0) (sum_vec_non_nil _ Hnnil)) with a by (apply Rpos_eq; simpl; nra).
    auto.
  - assert (b :: r <> nil) as H by now auto.
    specialize (IHr A H).
    change (sem_seq (vec (a :: b :: r) A)) with (a *S A +S (sem_seq (vec (b :: r) A))).
    replace (existT (fun r0 : R => (0 <? r0) = true) (sum_vec (a :: b :: r)) (sum_vec_non_nil _ Hnnil)) with (plus_pos a (existT _ (sum_vec (b :: r)) (sum_vec_non_nil _ H))) by (destruct a; destruct  b; apply Rpos_eq; simpl; nra).
    rewrite IHr.
    auto with MGA_solver.
Qed.

Lemma sem_seq_permutation : forall T1 T2, Permutation_Type T1 T2 -> sem_seq T1 === sem_seq T2.
Proof.
  intros T1 T2 Hperm; induction Hperm; try destruct x; try destruct y; simpl; try auto with MGA_solver.
  - rewrite 2? asso_plus.
    rewrite (commu_plus (r0 *S t0)); reflexivity.
  - transitivity (sem_seq l'); assumption.
Qed.

Lemma mul_vec_eq : forall A l r, sem_seq (vec (mul_vec r l) A) === r *S sem_seq (vec l A).
Proof.
  intros A.
  induction l; intros r.
  - simpl; rewrite mul_0; auto.
  - simpl.
    rewrite IHl.
    rewrite <-mul_assoc.
    rewrite mul_distri_term.
    reflexivity.
Qed.

(** ** Interpretation of a hypersequent *)
Fixpoint sem_hseq G :=
  match G with
  | nil => HR_zero (* should not happen *)
  | T1 :: nil => sem_seq T1
  | T1 :: G => (sem_seq T1) \/S (sem_hseq G)
  end.

(** *** Properties of this interpretation *)
Lemma sem_hseq_permutation : forall G1 G2, Permutation_Type G1 G2 -> sem_hseq G1 === sem_hseq G2.
Proof.
  intros G1 G2 Hperm; induction Hperm.
  - reflexivity.
  - destruct l; destruct l'.
    + reflexivity.
    + exfalso; apply (Permutation_Type_nil_cons Hperm).
    + apply Permutation_Type_sym in Hperm.
      exfalso; apply (Permutation_Type_nil_cons Hperm).
    + unfold sem_hseq; fold (sem_hseq (s :: l)); fold (sem_hseq (s0 :: l')).
      rewrite IHHperm; reflexivity.
  - destruct l.
    + simpl; apply commu_max.
    + unfold sem_hseq; fold (sem_hseq (s :: l)); rewrite ?asso_max; rewrite (commu_max (sem_seq y)); reflexivity.
  - transitivity (sem_hseq l'); assumption.
Qed.

repo: riesz-logic


text:
Require Import Coq.Sets.Ensembles Bedrock.Platform.AutoSep.

Require Import Bedrock.Platform.Malloc Bedrock.Platform.Facade.examples.SeqF.

Module Type ADT.
  Parameter lseq : list W -> W -> HProp.
  Parameter lseq' : list W -> W -> HProp.

  Axiom lseq_fwd : forall ls c, lseq ls c ===> [| c <> 0 |] * [| freeable c 2 |]
    * Ex p, Ex junk, (c ==*> p, junk) * lseq' ls p.
  Axiom lseq_bwd : forall ls (c : W), ([| c <> 0 |] * [| freeable c 2 |]
    * Ex p, Ex junk, (c ==*> p, junk) * lseq' ls p) ===> lseq ls c.

  Axiom lseq'_empty_fwd : forall ls (c : W), c = 0
    -> lseq' ls c
    ===> [| ls = nil |].

  Axiom lseq'_empty_bwd : forall ls (c : W), c = 0
    -> [| ls = nil |] ===> lseq' ls c.

  Axiom lseq'_nonempty_fwd : forall ls (c : W), c <> 0
    -> lseq' ls c
    ===> Ex x, Ex ls', [| ls = x :: ls' |] * [| freeable c 2 |] * Ex p', (c ==*> x, p')
        * lseq' ls' p'.

  Axiom lseq'_nonempty_bwd : forall ls (c : W), c <> 0
    -> (Ex x, Ex ls', [| ls = x :: ls' |] * [| freeable c 2 |] * Ex p', (c ==*> x, p')
        * lseq' ls' p') ===> lseq' ls c.

  Axiom lseq'_cons_fwd : forall x ls (c : W),
    lseq' (x :: ls) c
    ===> [| c <> 0 |] * [| freeable c 2 |] * Ex p', (c ==*> x, p') * lseq' ls p'.
End ADT.

Module Adt : ADT.
  Open Scope Sep_scope.

  Fixpoint lseq' (ls : list W) (p : W) : HProp :=
    match ls with
      | nil => [| p = 0 |]
      | x :: ls' => [| p <> 0 |] * [| freeable p 2 |]
        * Ex p', (p ==*> x, p')
        * lseq' ls' p'
    end.

  Definition lseq (ls : list W) (c : W) : HProp :=
    [| c <> 0 |] * [| freeable c 2 |]
    * Ex p, Ex junk, (c ==*> p, junk) * lseq' ls p.

  Theorem lseq_fwd : forall ls c, lseq ls c ===> [| c <> 0 |] * [| freeable c 2 |]
    * Ex p, Ex junk, (c ==*> p, junk) * lseq' ls p.
    unfold lseq; sepLemma.
  Qed.

  Theorem lseq_bwd : forall ls (c : W), ([| c <> 0 |] * [| freeable c 2 |]
    * Ex p, Ex junk, (c ==*> p, junk) * lseq' ls p) ===> lseq ls c.
    unfold lseq; sepLemma.
  Qed.

  Theorem lseq'_empty_fwd : forall ls (c : W), c = 0
    -> lseq' ls c
    ===> [| ls = nil |].
    destruct ls; sepLemma.
  Qed.

  Theorem lseq'_empty_bwd : forall ls (c : W), c = 0
    -> [| ls = nil |] ===> lseq' ls c.
    destruct ls; sepLemma.
  Qed.

  Theorem lseq'_nonempty_fwd : forall ls (c : W), c <> 0
    -> lseq' ls c
    ===> Ex x, Ex ls', [| ls = x :: ls' |] * [| freeable c 2 |] * Ex p', (c ==*> x, p')
        * lseq' ls' p'.
    destruct ls; sepLemma.
  Qed.

  Theorem lseq'_nonempty_bwd : forall ls (c : W), c <> 0
    -> (Ex x, Ex ls', [| ls = x :: ls' |] * [| freeable c 2 |] * Ex p', (c ==*> x, p')
        * lseq' ls' p') ===> lseq' ls c.
    destruct ls; sepLemma.
    injection H0; sepLemma.
  Qed.

  Theorem lseq'_cons_fwd : forall x ls (c : W),
    lseq' (x :: ls) c
    ===> [| c <> 0 |] * [| freeable c 2 |] * Ex p', (c ==*> x, p') * lseq' ls p'.
    sepLemma.
  Qed.
End Adt.

Import Adt.
Export Adt.

Definition hints : TacPackage.
  prepare (lseq_fwd, lseq'_empty_fwd, lseq'_nonempty_fwd, lseq'_cons_fwd)
  (lseq_bwd, lseq'_empty_bwd, lseq'_nonempty_bwd).
Defined.

Definition newS := newS lseq 8.
Definition deleteS := deleteS lseq 7.
Definition popS := popS lseq 8.
Definition emptyS := emptyS lseq 0.
Definition pushS := pushS lseq 8.
Definition copyS := copyS lseq 10.
Definition revS := revS lseq 2.
Definition lengthS := lengthS lseq 1.

Definition m := bimport [[ "malloc"!"malloc" @ [mallocS], "malloc"!"free" @ [freeS] ]]
  bmodule "ListSeq" {{
    bfunction "new"("extra_stack", "x") [newS]
      "x" <-- Call "malloc"!"malloc"(0, 2)
      [PRE[_, R] R =?> 2 * [| R <> 0 |] * [| freeable R 2 |] * mallocHeap 0
       POST[R'] lseq nil R' * mallocHeap 0];;

      "x" *<- 0;;
      Return "x"
    end

    with bfunction "delete"("extra_stack", "self", "ls") [deleteS]
      "ls" <-* "self";;

      Call "malloc"!"free"(0, "self", 2)
      [Al s,
        PRE[V] lseq' s (V "ls") * mallocHeap 0
        POST[R] [| R = $0 |] * mallocHeap 0];;

      [Al s,
        PRE[V] lseq' s (V "ls") * mallocHeap 0
        POST[R] [| R = $0 |] * mallocHeap 0]
      While ("ls" <> 0) {
        "self" <-* "ls"+4;;
        Call "malloc"!"free"(0, "ls", 2)
        [Al s,
          PRE[V] lseq' s (V "self") * mallocHeap 0
          POST[R] [| R = $0 |] * mallocHeap 0];;

        "ls" <- "self"
      };;

      Return 0
    end

    with bfunction "pop"("extra_stack", "self", "tmp", "r") [popS]
      "tmp" <-* "self";;
      "r" <-* "tmp";;
      "extra_stack" <-* "tmp"+4;;
      "self" *<- "extra_stack";;

      Call "malloc"!"free"(0, "tmp", 2)
      [PRE[V] Emp
       POST[R] [| R = V "r" |] ];;

      Return "r"
    end

    with bfunction "empty"("extra_stack", "self") [emptyS]
      "self" <-* "self";;

      If ("self" = 0) {
        Return 1
      } else {
        Return 0
      }
    end

    with bfunction "push"("extra_stack", "self", "n", "tmp") [pushS]
      "tmp" <-- Call "malloc"!"malloc"(0, 2)
      [Al p,
       PRE[V, R] V "self" =*> p * R =?> 2
       POST[R'] [| R' = $0 |] * V "self" =*> R * (R ==*> V "n", p) ];;

      "tmp" *<- "n";;
      "extra_stack" <-* "self";;
      "tmp"+4 *<- "extra_stack";;
      "self" *<- "tmp";;
      Return 0
    end

    with bfunction "copy"("extra_stack", "self", "new", "acc", "tmp") [copyS]
      "self" <-* "self";;

      "new" <-- Call "malloc"!"malloc"(0, 2)
      [Al ls,
       PRE[V, R] lseq' ls (V "self") * R =?> 1 * mallocHeap 0
       POST[R'] [| R' = R |] * lseq' ls (V "self") * Ex p, R =*> p * lseq' ls p * mallocHeap 0];;
      "acc" <- "new";;

      [Al ls,
       PRE[V] lseq' ls (V "self") * V "acc" =?> 1 * mallocHeap 0
       POST[R] [| R = V "new" |] * lseq' ls (V "self") * Ex p, V "acc" =*> p * lseq' ls p * mallocHeap 0]
      While ("self" <> 0) {
        "tmp" <-* "self";;
        "self" <-* "self"+4;;

        "extra_stack" <-- Call "malloc"!"malloc"(0, 2)
        [Al ls,
         PRE[V, R] R =?> 2 * [| R <> 0 |] * [| freeable R 2 |]
                 * lseq' ls (V "self") * V "acc" =?> 1 * mallocHeap 0
         POST[R'] [| R' = V "new" |] * lseq' ls (V "self") * Ex p, V "acc" =*> p
                * lseq' (V "tmp" :: ls) p * mallocHeap 0];;

        "acc" *<- "extra_stack";;
        "extra_stack" *<- "tmp";;
        "acc" <- "extra_stack"+4
      };;

      "acc" *<- 0;;
      Return "new"
    end

    with bfunction "length"("extra_stack", "self", "acc") [lengthS]
      "self" <-* "self";;
      "acc" <- 0;;

      [Al ls,
       PRE[V] lseq' ls (V "self")
       POST[R] [| R = V "acc" ^+ $ (length ls) |] * lseq' ls (V "self") ]
      While ("self" <> 0) {
        "acc" <- "acc" + 1;;
        "self" <-* "self"+4
      };;

      Return "acc"
    end with bfunction "rev"("extra_stack", "self", "from", "to") [revS]
      "from" <-* "self";;
      "to" <- 0;;

      [Al ls, Al ls',
       PRE[V] V "self" =?> 1 * lseq' ls (V "from") * lseq' ls' (V "to")
       POST[R] [| R = $0 |] * Ex p, V "self" =*> p * lseq' (rev_append ls ls') p]
      While ("from" <> 0) {
        "extra_stack" <-* "from"+4;;
        "from"+4 *<- "to";;
        "to" <- "from";;
        "from" <- "extra_stack"
      };;

      "self" *<- "to";;
      Return 0
    end
  }}.

Local Hint Extern 1 (@eq W _ _) => words.

Theorem ok : moduleOk m.
  vcgen; abstract (sep hints; eauto; try rewrite natToW_S; try rewrite <- rev_alt;
                   eauto; step auto_ext).
Qed.

author: mit-plv

repo: bedrock

save_path: github-repos/coq/mit-plv-bedrock


(* Define a function that takes a tuple of natural numbers (a,b) and returns
  the sum of the squares of both numbers. *)

Definition sum_square (a b : nat) := a * a + b * b.

Eval compute in sum_square 2 3.

(* Define a function that computes the sum of all squares between 1 and n,
  as a natural number.  Use the Fixpoint approach as described in the slides. *)

Fixpoint sum_n_square(n : nat) :=
   match n with
      0 => 0
    | S p => n*n + sum_n_square p end.

Eval compute in sum_n_square 3.

(* Write a function that maps any positive integer n to the list 1 ... n *)
(* Use the iter function shown in the slides. *)
(* Usage :
   iter n f a (for n : Z) computes f (f (f  ... a)) (n times)

   example:

Eval compute in iter 10 Z (fun i => 2* i) 1.
   = 1024
     : Z

*)
Require Import ZArith.
Open Scope Z_scope.

Require Import List.

Definition iota (n:Z) :=
 snd(
  iter n  (Z * (list Z))
	(fun p => match p with (last, l) => (last-1, last::l) end)
        (n,nil)).

Eval compute in (iota 4).

Eval compute in snd (3, (1::2::nil)).

Eval compute in iter 3 (Z * (list Z))
   (fun nl => match nl with (n, l) => (n-1, n::l) end)
   (3, nil).

(* Write a function that maps any n and any list a_1::...::a_p::nil
  to the list (n*a_1::...n*a_p::nil) *)

Fixpoint mult_list(n : Z)(l : list Z) : list Z :=
   match l with
       nil => nil
     | el::rl => let res := mult_list n rl in ((n*el)::res) end.

Eval compute in mult_list 3 (1::2::3::nil).

Definition mult_list_2 (n : Z)(l : list Z) : list Z :=
   (map
      (fun x => n*x)
      l
   ).

Eval compute in mult_list_2 3 (1::2::3::nil).

(* Hint use the map functional (slide 22) *)

(* Write a function that maps any n and any list l and returns the boolean
  value that indicates whether n is in l.
   You may use the function fold_right given in the slides and a
   function Zeq_bool  to compare two integers *)

Fixpoint is_in_l (l : list Z)(a : Z) : bool :=
   match l with
      nil => false
    | x::rl => if(Zeq_bool x a)
                 then true
                 else (is_in_l rl a) end.

Eval compute in is_in_l (1::2::3::nil) 1.

(* Write a function that checks whether n divides p, assuming n and p
   are both positive.  Here's a plan:
   build the list n::2*n::...::p*n::nil,
   check whether p is in this list. *)

Definition n_div_p (n:Z)(p:Z) : bool :=
   (is_in_l
      (mult_list n (iota p))
      p
   ).

Eval compute in n_div_p 6 18.

(* Write a function that checks whether n is prime. *)

Fixpoint is_prime_anex (n:Z)(l:list Z) : bool :=
   match l with
    nil => true
  | x::rl => if(n_div_p x n)
		then false
		else (is_prime_anex n rl) end.

Definition is_prime(n:Z) : bool :=
   match (iota (n-1)) with
      p::rl => is_prime_anex n rl
     |nil => true end.

Eval compute in is_prime 1.