text:
(**************************************************************)
(*   Copyright Dominique Larchey-Wendling [*]                 *)
(*                                                            *)
(*                             [*] Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

Require Import Arith Omega List Permutation Relations.

Require Import tacs.

Require Import rel_utils.

Require Import list_perm.
Require Import list_in.
Require Import list_prefix.

Set Implicit Arguments.

(* Forall tools *)

Section Forall.

  Variables (X : Type) (P : X -> Prop).

  Fact Forall_app ll mm : Forall P (ll++mm) <-> Forall P ll /\ Forall P mm.
  Proof.
    split.
    induction ll as [ | x ll ]; split; auto.
    constructor;
    inversion H; auto.
    apply IHll; auto.
    inversion H; apply IHll; auto.
    intros (H1 & H2).
    induction H1; simpl; auto; constructor; auto.
  Qed.

  Fact Forall_cons_inv x ll : Forall P (x::ll) <-> P x /\ Forall P ll.
  Proof.
    split.
    inversion_clear 1; auto.
    constructor; tauto.
  Qed.

End Forall.

Section Forall_rect.

  Variables (X : Type) (P : X -> Prop) (Q : list X -> Type)
            (HP1 : Q nil)
            (HP2 : forall x l, P x -> Forall P l -> Q l -> Q (x::l)).

  Fact Forall_rect l : Forall P l -> Q l.
  Proof.
    induction l as [ | x l IHl ].
    intros _; apply HP1.
    intros H; apply Forall_cons_inv in H; destruct H.
    apply HP2; auto.
  Qed.

End Forall_rect.

Section Forall_Permutation.

  Variables (X : Type) (P : X -> Prop).

  Let Forall_perm_rec ll mm : ll ~p mm -> Forall P ll -> Forall P mm.
  Proof.
    induction 1; auto.
    intros G; constructor; inversion_clear G; auto.
    intros G.
    apply Forall_cons_inv in G; destruct G as [ Gy G ].
    apply Forall_cons_inv in G; destruct G as [ Gx G ].
    repeat constructor; auto.
  Qed.

  Fact Forall_perm ll mm : ll ~p mm -> (Forall P ll <-> Forall P mm).
  Proof.
    split; apply Forall_perm_rec; auto.
    apply Permutation_sym; auto.
  Qed.

End Forall_Permutation.

Section map_ext_Forall.

  Variable (X Y : Type) (f g : X -> Y).

  Fact map_ext_Forall ll : (Forall (fun x => f x = g x) ll) -> map f ll = map g ll.
  Proof.
    induction 1; simpl; f_equal; auto.
  Qed.

  Variable P : Y -> Prop.

  Fact Forall_map ll : Forall P (map f ll) <-> Forall (fun x => P (f x)) ll.
  Proof.
    split.
    induction ll as [ | x ll IH ]; constructor;
    simpl in H; inversion_clear H; auto.
    induction 1; constructor; auto.
  Qed.

End map_ext_Forall.

Section Forall_flat_map.

  Variable (A B C D : Type) (f f' : A -> list B) (P : B -> Prop).

  Fact Forall_flat_map ll : Forall P (flat_map f ll) <-> Forall (fun x => Forall P (f x)) ll.
  Proof.
    split.

    induction ll as [ | x ll IH ].
    constructor.
    simpl; intros H.
    rewrite Forall_app in H.
    constructor; try apply H.
    apply IH, H.

    induction 1; simpl.
    constructor.
    rewrite Forall_app; split; auto.
  Qed.

End Forall_flat_map.

(* Forall2 tools *)

Fact list_length_eq_Forall2 X Y (l : list X) (m : list Y) : length l = length m <-> Forall2 (fun _ _ => True) l m.
Proof.
  split.
  revert m; induction l; intros [|]; try discriminate 1; simpl; intros H; constructor; auto.
  induction 1; simpl; f_equal; auto.
Qed.

Fact Forall2_nil_inv_l X Y R m : @Forall2 X Y R nil m -> m = nil.
Proof.
  inversion_clear 1; reflexivity.
Qed.

Fact Forall2_nil_inv_r X Y R m : @Forall2 X Y R m nil -> m = nil.
Proof.
  inversion_clear 1; reflexivity.
Qed.

Fact Forall2_cons_inv X Y R x l y m : @Forall2 X Y R (x::l) (y::m) <-> R x y /\ Forall2 R l m.
Proof.
  split.
  inversion_clear 1; auto.
  intros []; constructor; auto.
Qed.

Fact Forall2_app_inv_l X Y R l1 l2 m :
    @Forall2 X Y R (l1++l2) m -> { m1 : _ & { m2 | Forall2 R l1 m1 /\ Forall2 R l2 m2 /\ m = m1++m2 } }.
Proof.
  revert l2 m;
  induction l1 as [ | x l1 IH ]; simpl; intros l2 m H.
  exists nil, m; repeat split; auto.
  destruct m as [ | y m ].
  apply Forall2_nil_inv_r in H; discriminate H.
  apply Forall2_cons_inv in H; destruct H as [ H1 H2 ].
  apply IH in H2.
  destruct H2 as (m1 & m2 & H2 & H3 & H4); subst m.
  exists (y::m1), m2; repeat split; auto.
Qed.

Fact Forall2_app_inv_r X Y R l m1 m2 :
    @Forall2 X Y R l (m1++m2) -> { l1 : _ & { l2 | Forall2 R l1 m1 /\ Forall2 R l2 m2 /\ l = l1++l2 } }.
Proof.
  revert m2 l;
  induction m1 as [ | y m1 IH ]; simpl; intros m2 l H.
  exists nil, l; repeat split; auto.
  destruct l as [ | x l ].
  apply Forall2_nil_inv_l in H; discriminate H.
  apply Forall2_cons_inv in H; destruct H as [ H1 H2 ].
  apply IH in H2.
  destruct H2 as (l1 & l2 & H2 & H3 & H4); subst l.
  exists (x::l1), l2; repeat split; auto.
Qed.

Fact Forall2_cons_inv_l X Y R a ll mm :
      @Forall2 X Y R (a::ll) mm
   -> { b : _ & { mm' | R a b /\ mm = b::mm' /\ Forall2 R ll mm' } }.
Proof.
  intros H.
  apply Forall2_app_inv_l with (l1 := a::nil) (l2 := ll) in H.
  destruct H as (l & mm' & H1 & H2 & H3).
  destruct l as [ | y l ].
  exfalso; inversion H1.
  apply Forall2_cons_inv in H1.
  destruct H1 as [ H1 H4 ].
  apply Forall2_nil_inv_l in H4; subst l.
  exists y, mm'; auto.
Qed.

Fact Forall2_cons_inv_r X Y R b ll mm :
      @Forall2 X Y R ll (b::mm)
   -> { a : _ & { ll' | R a b /\ ll = a::ll' /\ Forall2 R ll' mm } }.
Proof.
  intros H.
  apply Forall2_app_inv_r with (m1 := b::nil) (m2 := mm) in H.
  destruct H as (l & ll' & H1 & H2 & H3).
  destruct l as [ | x l  ].
  exfalso; inversion H1.
  apply Forall2_cons_inv in H1.
  destruct H1 as [ H1 H4 ].
  apply Forall2_nil_inv_r in H4; subst l.
  exists x, ll'; auto.
Qed.

Fact Forall2_rev X Y (R : X -> Y -> Prop) ll mm : Forall2 R ll mm <-> Forall2 R (rev ll) (rev mm).
Proof.
  assert (forall ll mm, Forall2 R ll mm -> Forall2 R (rev ll) (rev mm)) as H.
    induction 1; simpl; auto.
    apply Forall2_app; auto.
  split; auto.
  rewrite <- (rev_involutive ll) at 2.
  rewrite <- (rev_involutive mm) at 2.
  auto.
Qed.

Fact Forall2_conj X Y (R S : X -> Y -> Prop) ll mm : Forall2 (fun x y => R x y /\ S x y) ll mm <-> Forall2 R ll mm /\ Forall2 S ll mm.
Proof.
  split.
  induction 1; split; constructor; tauto.
  intros [H1 H2]; revert H1 H2.
  induction 1 as [ | x ll y mm H1 H2 IH ]; intros H; auto.
  apply Forall2_cons_inv in H; constructor; tauto.
Qed.

Fact Forall2_map_left X Y Z (R : Y -> X -> Prop) (f : Z -> Y) ll mm : Forall2 R (map f ll) mm <-> Forall2 (fun x y => R (f x) y) ll mm.
Proof.
  split.
  revert mm.
  induction ll; intros [ | y mm ] H; simpl in H; auto; try (inversion H; fail).
  apply Forall2_cons_inv in H; constructor.
  tauto.
  apply IHll; tauto.
  induction 1; constructor; auto.
Qed.

Fact Forall2_map_right X Y Z (R : Y -> X -> Prop) (f : Z -> X) mm ll : Forall2 R mm (map f ll) <-> Forall2 (fun y x => R y (f x)) mm ll.
Proof.
  split.
  revert mm.
  induction ll; intros [ | y mm ] H; simpl in H; auto; try (inversion H; fail).
  apply Forall2_cons_inv in H; constructor.
  tauto.
  apply IHll; tauto.
  induction 1; constructor; auto.
Qed.

Fact Forall2_map_both X Y X' Y' (R : X -> Y -> Prop) (f : X' -> X) (g : Y' -> Y) ll mm : Forall2 R (map f ll) (map g mm) <-> Forall2 (fun x y => R (f x) (g y)) ll mm.
Proof.
  rewrite Forall2_map_left, Forall2_map_right; split; auto.
Qed.

Fact Forall2_Forall X (R : X -> X -> Prop) ll : Forall2 R ll ll <-> Forall (fun x => R x x) ll.
Proof.
  split.
  induction ll as [ | x ll ]; inversion_clear 1; auto.
  induction 1; auto.
Qed.

Fact Forall2_map_Forall X Y (R : Y -> X -> Prop) (f : X -> Y) ll : Forall2 R (map f ll) ll <-> Forall (fun x => R (f x) x) ll.
Proof.
  rewrite Forall2_map_left, Forall2_Forall; split; auto.
Qed.

Fact Forall2_exchg X Y (R : X -> Y -> Prop) ll mm : Forall2 R ll mm <-> Forall2 (fun y x => R x y) mm ll.
Proof.
  split; induction 1; constructor; tauto.
Qed.

Section Forall2_comp.

  Variable (X Y Z : Type) (R : X -> Y -> Prop) (S : Y -> Z -> Prop).

  Fact Forall2_compose k l m : Forall2 R k l -> Forall2 S l m
                            -> Forall2 (fun x z => exists y, R x y /\ S y z) k m.
  Proof.
    intros H; revert H m.
    induction 1 as [ | x y k l H1 H2 H3 ]; intros [ | z m ] H4.
    constructor.
    inversion H4.
    inversion H4.
    apply Forall2_cons_inv in H4.
    destruct H4 as (H4 & H5).
    constructor; auto.
    exists y; auto.
  Qed.

End Forall2_comp.

Fact Forall2_length X Y (R : X -> Y -> Prop) ll mm : Forall2 R ll mm -> length ll = length mm.
Proof.
  induction 1; simpl; f_equal; auto.
Qed.

Fact Forall2_eq X ll mm : Forall2 (@eq X) ll mm <-> ll = mm.
Proof.
  split.
  induction 1; f_equal; auto.
  intros; subst; apply Forall2_Forall.
  induction mm; simpl; auto.
Qed.

Fact Forall2_In_inv_left X Y (R : X -> Y -> Prop) ll mm : Forall2 R ll mm -> forall x, In x ll -> exists y, In y mm /\ R x y.
Proof.
  induction 1 as [ | a b ll mm H1 H2 IH2 ].
  intros ? [].
  intros x [ Hx | Hx ]; subst.
  exists b; simpl; auto.
  destruct (IH2 _ Hx) as (y & H3 & H4).
  exists y; simpl; auto.
Qed.

Fact Forall2_In_inv_right X Y (R : X -> Y -> Prop) ll mm : Forall2 R ll mm -> forall y, In y mm -> exists x, In x ll /\ R x y.
Proof.
  induction 1 as [ | a b ll mm H1 H2 IH2 ].
  intros ? [].
  intros x [ Hx | Hx ]; subst.
  exists a; simpl; auto.
  destruct (IH2 _ Hx) as (y & H3 & H4).
  exists y; simpl; auto.
Qed.

Fact Forall2_impl_Forall2_incl X Y (R S : X -> Y -> Prop) ll mm :
      Forall2 (fun x y => R x y -> S x y) ll mm
   -> Forall2 R ll mm -> Forall2 S ll mm.
Proof.
  induction 1 as [ | x y ll mm H1 H2 H3 ]; simpl.
  intros; constructor.
  intros H; apply Forall2_cons_inv in H.
  constructor; tauto.
Qed.

Fact Forall2_impl X Y (R S : X -> Y -> Prop) : R inc2 S -> Forall2 R inc2 Forall2 S.
Proof. intros ? ? ?; induction 1; constructor; auto. Qed.

Fact Forall2_True X Y (R : X -> Y -> Prop) : (forall x y, R x y) -> forall ll mm, length ll = length mm -> Forall2 R ll mm.
Proof.
  intros HR.
  induction ll as [ | x ll IH ]; intros [ | y mm ]; try discriminate 1; intros H.
  constructor.
  injection H; clear H; intros H.
  constructor; auto.
Qed.

Fact Forall2_incl_map X Y (f : list X -> list Y) l m :
       (forall u v, incl u v -> incl (f u) (f v))
    -> Forall2 (@incl _) l m
    -> Forall2 (@incl _) (map f l) (map f m).
Proof.
  intro; induction 1; simpl; constructor; auto.
Qed.

Fact Forall2_comp X Y Z (R : X -> Y -> Prop) (S : Y -> Z -> Prop) : Forall2 R o Forall2 S inc2 Forall2 (R o S).
Proof.
  intros ? ? (mm & ? & ?); apply Forall2_compose with mm; auto.
Qed.

Fact Forall2_pfx A B (R : A -> B -> Prop) f g n : Forall2 R (pfx f n) (pfx g n) <-> forall i, i < n -> R (f i) (g i).
Proof.
  revert f g;
  induction n as [ | n IHn ]; intros f g; simpl.
  split; intros; auto; omega.
  split.
  intros H.
  apply Forall2_cons_inv in H.
  destruct H as [ H1 H2 ].
  intros [ | i ]; auto.
  intros; apply IHn with (f := fun n => f (S n)) (g := fun n => g (S n)); auto; omega.
  intros H; constructor.
  apply H; omega.
  apply IHn with (f := fun n => f (S n)) (g := fun n => g (S n)).
  intros; apply H; omega.
Qed.

Section Forall2_tools.

  Variables (X Y : Type) (P : X -> Prop) (Q : Y -> Prop) (R S : relation X) (T : X -> Y -> Prop).

  Fact Forall2_Forall_left ll mm : Forall2 (fun x y => P x -> T x y) ll mm -> Forall P ll -> Forall2 T ll mm.
  Proof.
    induction 1 as [ | x y ll mm H1 IH ]; intros H2.
    constructor.
    apply Forall_cons_inv in H2; destruct H2.
    constructor; auto.
  Qed.

  Fact Forall2_Forall_right ll mm : Forall2 (fun x y => Q y -> T x y) ll mm -> Forall Q mm -> Forall2 T ll mm.
  Proof.
    induction 1 as [ | x y ll mm H1 IH ]; intros H2.
    constructor.
    apply Forall_cons_inv in H2; destruct H2.
    constructor; auto.
  Qed.

  Fact Forall_Forall2 ll : Forall (fun x => R x x) ll <-> Forall2 R ll ll.
  Proof.
    split.
    induction 1; constructor; auto.
    induction ll; intros H; constructor; inversion_clear H; auto.
  Qed.

  Fact Forall2_sym : symmetric _ R -> symmetric _ (Forall2 R).
  Proof. intros ? ? ?; induction 1; auto. Qed.

  Fact Forall2_trans : transitive _ R -> transitive _ (Forall2 R).
  Proof.
    intros HR ll mm kk H1; revert kk.
    induction H1 as [ | x y ll mm H1 H2 IH ]; intros kk H3; auto.
    inversion_clear H3; constructor; auto.
    apply HR with (1 := H1); auto.
  Qed.

  Fact Forall2_Forall_Forall ll mm :
         (forall x y, T x y -> P x -> Q y)
      -> Forall2 T ll mm
      -> Forall P ll
      -> Forall Q mm.
    Proof.
      intros H.
      induction 1 as [ | x y ll mm H1 H2 IH2 ]; intros Hll.
      constructor.
      apply Forall_cons_inv in Hll; destruct Hll as [ Hx Hll ].
      constructor; auto.
      revert Hx; apply H; auto.
    Qed.

  Fact Forall2_perm_comm ll mm kk : Forall2 R ll mm -> Permutation mm kk -> exists ll', Permutation ll ll' /\ Forall2 R ll' kk.
  Proof.
    intros H1; revert kk.
    induction H1; intros kk Hkk.
    apply Permutation_nil in Hkk; subst.
    exists nil; auto.
    destruct Permutation_In_inv with (1 := Hkk) (x := y) as (l'' & r'' & ?); subst.
    left; auto.
    apply Permutation_app_inv with (l1 := nil) in Hkk; simpl in Hkk.
    apply IHForall2 in Hkk.
    destruct Hkk as (l1 & H2 & H3).
    apply Forall2_app_inv_r in H3.
    destruct H3 as (l2 & l3 & H3 & H4 & ?); subst.
    exists (l2++x::l3); split.
    apply Permutation_add_one with (l1 := nil); auto.
    apply Forall2_app; auto.
  Qed.

  Variable (f : X -> list Y).

  Fact Forall2_In_map_impl ll mm ts :
              Forall2 (fun x y => forall t, In x (f t) -> In y (f t)) ll mm
           -> Forall2 (@In _) ll (map f ts)
           -> Forall2 (@In _) mm (map f ts).
  Proof.
    intros H; revert ts.
    induction H.
    auto.
    intros [ | t ts ].
    inversion 1.
    simpl.
    inversion_clear 1; constructor; auto.
  Qed.

End Forall2_tools.

Fact Forall2_left_Forall X Y (P : X -> Prop) lx ly : Forall2 (fun x (_ : Y) => P x) lx ly <-> Forall P lx /\ length lx = length ly.
Proof.
  split.
  intros H; split.
  induction H; constructor; auto.
  revert H; apply Forall2_length.
  intros (H1 & H2); revert ly H2.
  induction H1; intros [ | ] H2; try discriminate H2; constructor; auto.
Qed.

Fact Forall2_right_Forall X Y (P : Y -> Prop) lx ly : Forall2 (fun (_ : X) y => P y) lx ly <-> Forall P ly /\ length lx = length ly.
Proof.
  split.
  intros H; split.
  induction H; constructor; auto.
  revert H; apply Forall2_length.
  intros (H1 & H2); revert lx H2.
  induction H1; intros [ | ] H2; try discriminate H2; constructor; auto.
Qed.

Fact Forall2_cond_left X Y (P : X -> Prop) (R : X -> Y -> Prop) ll mm :
  Forall P ll -> Forall2 (fun x y => P x -> R x y) ll mm -> Forall2 R ll mm.
Proof.
  intros H1 H2.
  apply (Forall2_impl_Forall2_incl _ H2).
  apply Forall2_left_Forall; split; auto.
  apply Forall2_length with (1 := H2).
Qed.

Fact Forall2_cond_right X Y (P : Y -> Prop) (R : X -> Y -> Prop) ll mm :
  Forall P mm -> Forall2 (fun x y => P y -> R x y) ll mm -> Forall2 R ll mm.
Proof.
  intros H1 H2.
  apply (Forall2_impl_Forall2_incl _ H2).
  apply Forall2_right_Forall; split; auto.
  apply Forall2_length with (1 := H2).
Qed.

Fact map_eq_Forall2 X Y Z (g1 : X -> Z) (g2 : Y -> Z) ll mm : map g1 ll = map g2 mm <-> Forall2 (fun x y => g1 x = g2 y) ll mm.
Proof.
  split.
  revert mm.
  induction ll as [ | x ll IH ]; intros [ | y mm ]; intros H; try discriminate H;
  constructor.
  injection H; auto.
  apply IH.
  injection H; auto.
  induction 1; simpl; f_equal; auto.
Qed.

Fact Forall2_list_In_map X Y Z (R : Y -> Z -> Prop) ll f g : (forall (x : X) (H : In x ll), R (f x H) (g x H)) <-> Forall2 R (list_In_map ll f) (list_In_map ll g).
Proof.
  split.
  induction ll; simpl; auto.
  revert f g;
  induction ll; simpl; intros f g.
  intros _ _ [].
  intros H.
  apply Forall2_cons_inv in H.
  destruct H as ( H1 & H2 ).
  intros x [ Hx | Hx ].
  subst x; auto.
  apply IHll with (1 := H2).
Qed.

Fact Forall2_list_In_t_map X Y Z (R : Y -> Z -> Prop) ll f g : (forall (x : X) (H : In_t x ll), R (f x H) (g x H)) <-> Forall2 R (list_In_t_map ll f) (list_In_t_map ll g).
Proof.
  split.
  induction ll; simpl; auto.
  revert f g;
  induction ll; simpl; intros f g.
  intros _ _ [].
  intros H.
  apply Forall2_cons_inv in H.
  destruct H as ( H1 & H2 ).
  intros x [ Hx | Hx ].
  subst x; auto.
  apply IHll with (1 := H2).
Qed.

Fact Forall2_to_list_In_t_map X Y (R : X -> Y -> Prop) l m :
          Forall2 R l m
       -> { f : forall x, In_t x l -> Y
              | m = list_In_t_map l f
             /\ forall x Hx, R x (f x Hx) }.
Proof.
  revert m.
  induction l as [ | x l IH ]; intros [ | y m ] H; try (exfalso; inversion H; fail).
  exists (fun x Hx => @False_rect _ Hx); split; auto; intros ? [].
  apply Forall2_cons_inv in H; destruct H as (H1 & H2).
  destruct (IH _ H2) as (f & Hf1 & Hf2).
  exists (fun x Hx => match Hx with inl _ => y | inr Hx => f _ Hx end); split.
  simpl; f_equal; apply Hf1.
  intros z [ Hz | Hz ]; simpl.
  subst; auto.
  apply Hf2.
Qed.

Fact Forall2_combine X Y (R : X -> Y -> Prop) l m :
          Forall2 R l m -> Forall (fun c => R (fst c) (snd c)) (combine l m).
Proof.
  induction 1; simpl; constructor; auto.
Qed.

Fact Forall2_combine_In X Y (R : X -> Y -> Prop) l m :
          Forall2 R l m -> forall x, In x l -> exists c, In c (combine l m) /\ fst c = x.
Proof.
  induction 1 as [ | x y l m H1 H2 IH2 ]; simpl; intros z.
  intros [].
  intros [ ? | H ].
  subst z; exists (x,y); tauto.
  destruct (IH2 _ H) as (c & H3 & H4).
  exists c; tauto.
Qed.

Section analysis_fun.

  Variable (X Y : Type) (P : X -> Prop) (f : X -> Y).

  Fact Forall2_analysis lx ly : Forall2 (fun x y => P x /\ f x = y) lx ly
                              <-> Forall P lx /\ map f lx = ly.
  Proof.
    rewrite Forall2_conj.
    rewrite Forall2_left_Forall.
    rewrite <- Forall2_map_left, Forall2_eq.
    split; try tauto.
    intros (? & ?); subst; rewrite map_length; auto.
  Qed.

End analysis_fun.

Section list_sup.

  Variables (X : Type)
            (P : nat -> X -> Prop) (P_mono : forall n x, P n x -> P (S n) x)
            (R : nat -> relation X) (R_mono : forall n, R n inc2 R (S n)).

  Let P_monotonic n m : n <= m -> forall x, P n x -> P m x.
  Proof.
    induction 1; intros; auto.
  Qed.

  Let R_monotonic n m : n <= m -> R n inc2 R m.
  Proof.
    induction 1; intros; auto.
  Qed.

  Fact list_Forall_sup ll : (forall x, In x ll -> exists n, P n x) -> exists n, forall x, In x ll -> P n x.
  Proof.
    induction ll as [ | x ll IH ]; intros H.
    exists 0; intros ? [].
    destruct (H x) as (n1 & H1).
    left; auto.
    destruct IH as (n2 & H2).
    intros; apply H; right; auto.
    exists (n1+n2); intros y [ Hy | Hy ].
    subst; revert H1; apply P_monotonic, le_plus_l.
    generalize (H2 _ Hy); apply P_monotonic, le_plus_r.
  Qed.

  Fact list_Forall2_mono Y Z (S T : Y -> Z -> Prop) : S inc2 T -> Forall2 S inc2 Forall2 T.
  Proof.
    intros ? ? ?; induction 1; constructor; auto.
  Qed.

  Fact list_Forall2_sup ll mm : Forall2 (fun x y => exists n, R n x y) ll mm -> exists n, Forall2 (R n) ll mm.
  Proof.
    induction 1 as [ | x y ll mm (n1 & H1) _ (n2 & IH2) ].
    exists 0; auto.
    exists (n1+n2); constructor.
    revert H1; apply R_monotonic, le_plus_l.
    revert IH2; apply list_Forall2_mono, R_monotonic, le_plus_r.
  Qed.

End list_sup.

Fact Forall2_w_continuous X K ll mm : @seq_increasing X K -> Forall2 (fun x y => exists n, K n x y) ll mm -> exists n, Forall2 (K n) ll mm.
Proof.
  intros HK.
  induction 1 as [ | x y ll mm (n & Hn) H2 (m & Hm) ].
  exists 0; constructor.
  exists (n+m); constructor.
  revert Hn; apply seq_inc_all; auto; omega.
  revert Hm; apply Forall2_impl, seq_inc_all; auto; omega.
Qed.

Section Exists2.

  Variable (X Y : Type) (R : X -> Y -> Prop).

  Inductive Exists2 : list X -> list Y -> Prop :=
    | Exists2_start : forall x y l m, R x y -> length l = length m -> Exists2 (x::l) (y::m)
    | Exists2_cont  : forall x y l m, Exists2 l m -> Exists2 (x::l) (y::m).

  Fact Exists2_length l m : Exists2 l m -> length l = length m.
  Proof.
    induction 1; simpl; auto.
  Qed.

  Fact Exists2_nil_inv : ~ Exists2 nil nil.
  Proof. inversion 1. Qed.

  Fact Exists2_cons_inv x y l m : Exists2 (x::l) (y::m) -> R x y \/ Exists2 l m.
  Proof.
    inversion_clear 1; tauto.
  Qed.

  Fact Exists2_In ll mm : Exists2 ll mm -> exists x y, In x ll /\ In y mm /\ R x y.
  Proof.
    induction 1 as [ x y | a b ll mm _ (x & y & H1 & H2 & H3) ].
    exists x, y; simpl; auto.
    exists x, y; simpl; auto.
  Qed.

End Exists2.

Fact Exists2_inc X Y (R S : X -> Y -> Prop) : R inc2 S -> Exists2 R inc2 Exists2 S.
Proof.
  intros H ll mm.
  induction 1.
  constructor 1; auto.
  constructor 2; auto.
Qed.

Fact Exists2_exists_left X Y R ll mm : @Exists2 X Y (fun x _ => R x) ll mm <-> length ll = length mm /\ exists x, In x ll /\ R x.
Proof.
  split.
  induction 1 as [ | x y l m H1 (H2 & z & H3 & H4) ].
  split.
  simpl; f_equal; auto.
  exists x; simpl; auto.
  split.
  simpl; f_equal; auto.
  exists z; simpl; auto.
  intros (H1 & x & H2 & H3).
  revert mm H1.
  induction ll as [ | z ll IH ].
  destruct H2.
  intros [ | y mm ] Hmm.
  discriminate Hmm.
  simpl in Hmm; injection Hmm; clear Hmm; intros Hmm.
  destruct H2 as [ H2 | H2 ].
  subst; constructor 1; auto.
  constructor 2; auto.
Qed.

Fact Exists2_exists_right X Y R ll mm : @Exists2 X Y (fun _ y => R y) ll mm <-> length ll = length mm /\ exists y, In y mm /\ R y.
Proof.
  split.
  induction 1 as [ | x y l m H1 (H2 & z & H3 & H4) ].
  split.
  simpl; f_equal; auto.
  exists y; simpl; auto.
  split.
  simpl; f_equal; auto.
  exists z; simpl; auto.
  intros (H1 & y & H2 & H3).
  revert ll H1.
  induction mm as [ | z mm IH ].
  destruct H2.
  intros [ | x ll ] Hll.
  discriminate Hll.
  simpl in Hll; injection Hll; clear Hll; intros Hll.
  destruct H2 as [ H2 | H2 ].
  subst; constructor 1; auto.
  constructor 2; auto.
Qed.

Section Forall2_Exists2.

  Variable (X Y : Type) (R S : X -> Y -> Prop).

  Fact Forall2_decide_ind ll mm : Forall2 (R cup2 S) ll mm -> Forall2 R ll mm \/ Exists2 S ll mm.
  Proof.
    induction 1 as [ | x y ll mm [ H1 | H1 ] H2 [ H3 | H3 ] ].
    left; constructor.
    left; constructor; auto.
    right; constructor 2; auto.
    right; constructor 1; auto.
    apply Forall2_length with (1 := H2); auto.
    right; constructor 2; auto.
  Qed.

End Forall2_Exists2.

Section Forall2_dec.

  Variable (X Y : Type).

  Implicit Types (R S : X -> Y -> Prop).

  Fact Forall2_choose_t R S ll mm : (forall x y, In_t x ll -> In_t y mm -> { R x y } + { S x y })
                           -> length ll = length mm -> { Forall2 R ll mm } + { Exists2 S ll mm }.
  Proof.
    revert mm.
    induction ll as [ | x ll IHll ]; intros [ | y mm ] HRS H.
    left; constructor.
    discriminate H.
    discriminate H.
    simpl in H; injection H; clear H; intros H.
    destruct (IHll mm) as [ H1 | H1 ]; auto.
    intros; apply HRS; right; auto.
    destruct (HRS x y); try (left; auto; fail).
    right; constructor 1; auto.
    right; constructor 2; auto.
  Qed.

  Fact Forall2_dec_t R ll mm :  (forall x y, In_t x ll -> In_t y mm -> { R x y } + { ~ R x y })
                           -> { Forall2 R ll mm } + { ~ Forall2 R ll mm }.
  Proof.
    intros H1.
    destruct (eq_nat_dec (length ll) (length mm)) as [ H2 | H2 ].
    destruct (Forall2_choose_t _ _ _ _ H1 H2) as [ | C ].
    left; auto.
    right; intros H.
    clear H1 H2.
    induction H.
    apply Exists2_nil_inv in C; auto.
    apply Exists2_cons_inv in C.
    destruct C; tauto.
    right; contradict H2; revert H2; apply Forall2_length.
  Qed.

  Fact Forall2_dec R ll mm :  (forall x y, In x ll -> In y mm -> { R x y } + { ~ R x y })
                           -> { Forall2 R ll mm } + { ~ Forall2 R ll mm }.
  Proof.
    intros H; apply Forall2_dec_t.
    intros; apply H; apply In_t_In; auto.
  Qed.

  Fact Exists2_dec_t R ll mm :  (forall x y, In_t x ll -> In_t y mm -> { R x y } + { ~ R x y })
                           -> { Exists2 R ll mm } + { ~ Exists2 R ll mm }.
  Proof.
    intros H1.
    destruct (eq_nat_dec (length ll) (length mm)) as [ H2 | H2 ].
    assert (forall x y, In_t x ll -> In_t y mm -> { ~ R x y } + { R x y }) as H3.
      intros x y Hx Hy; destruct (H1 _ _ Hx Hy); tauto.
    destruct (Forall2_choose_t _ _ _ _ H3 H2) as [ C | C ].

    right.
    clear H1 H2 H3.
    induction C as [ | a b ll mm H1 H2 H3 ].
    apply Exists2_nil_inv.
    contradict H3.
    apply Exists2_cons_inv in H3; tauto.

    left; auto.

    right.
    contradict H2; revert H2.
    apply Exists2_length.
  Qed.

  Fact Exists2_dec R ll mm :  (forall x y, In x ll -> In y mm -> { R x y } + { ~ R x y })
                           -> { Exists2 R ll mm } + { ~ Exists2 R ll mm }.
  Proof.
    intros H; apply Exists2_dec_t.
    intros; apply H; apply In_t_In; auto.
  Qed.

End Forall2_dec.

Section Forall3.

  Variable (X Y Z : Type).

  Implicit Type (R S : X -> Y -> Z -> Prop) (lx : list X).

  Inductive Forall3 R : list X -> list Y -> list Z -> Prop :=
    | in_Forall3_nil  : Forall3 R nil nil nil
    | in_Forall3_cons : forall x lx y ly z lz, R x y z
                                            -> Forall3 R lx ly lz
                                            -> Forall3 R (x::lx) (y::ly) (z::lz).

  Inductive Exists3 R : list X -> list Y -> list Z -> Prop :=
    | Exists3_start : forall x lx y ly z lz, R x y z
                                          -> length lx = length ly
                                          -> length lx = length lz
                                          -> Exists3 R (x::lx) (y::ly) (z::lz)
    | Exists3_cont : forall x lx y ly z lz, Exists3 R lx ly lz
                                         -> Exists3 R (x::lx) (y::ly) (z::lz).

  Fact Forall3_inc R S li : Forall (fun i => R i inc2 S i) li
                         -> Forall3 R li inc2 Forall3 S li.
  Proof.
    induction 1 as [ | i li H1 H2 ]; auto.
    intros [ | x lx ] [ | y ly ]; try (inversion 1; fail); constructor.
    intros [ | x lx ] [ | y ly ]; try (inversion 1; fail).
    inversion_clear 1.
    constructor; auto.
  Qed.

  Fact Forall3_length R lx ly lz : Forall3 R lx ly lz -> length lx = length ly /\ length lx = length lz.
  Proof.
    induction 1 as [ | x lx y ly z lz H1 H2 (H3 & H4) ]; simpl; auto.
  Qed.

  Fact Forall3_cup R S lx ly lz : Forall3 (fun i => R i cup2 S i) lx ly lz
                               -> Forall3 R lx ly lz \/ Exists3 S lx ly lz.
  Proof.
    induction 1 as [ | x lx y ly z lz H1 H2 H3 ].
    left; constructor.
    destruct H1; destruct H3.
    left; constructor; auto.
    right; constructor 2; auto.
    apply Forall3_length in H2; destruct H2.
    right; constructor 1; auto.
    right; constructor 2; auto.
  Qed.

  Fact Forall3_Forall2_first K lx ly lz : Forall3 (fun _ => K) lx ly lz
                                       -> Forall2 K ly lz.
  Proof.
    induction 1; simpl; constructor; auto.
  Qed.

  Fact Exists3_Exists2_last R lx ly lz :
                Exists3 R lx ly lz
             -> exists z, In z lz /\ Exists2 (fun x y => R x y z) lx ly.
  Proof.
    induction 1 as [ x lx y ly z lz H1 H2 H3
                   | x lx y ly z lz H1 H2 ].
    exists z; simpl; split; try tauto.
    constructor 1; auto.
    destruct H2 as (z' & H2 & H3).
    exists z'; simpl; split; try tauto.
    constructor 2; auto.
  Qed.

End Forall3.

author: DmxLarchey

repo: Relevant-decidability


text:
(* Default settings (from HsToCoq.Coq.Preamble) *)

Generalizable All Variables.

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

Require Coq.Program.Tactics.
Require Coq.Program.Wf.

(* Preamble *)

(* Converted imports: *)

Require Core.
Require Data.Tuple.
Require GHC.Base.
Import GHC.Base.Notations.

(* Converted type declarations: *)

Definition InterestingVarFun :=
  (Core.Var -> bool)%type.

Definition FV :=
  (InterestingVarFun ->
   Core.VarSet ->
   (list Core.Var * Core.VarSet)%type -> (list Core.Var * Core.VarSet)%type)%type.

(* Converted value declarations: *)

Definition unitFV : Core.Id -> FV :=
  fun arg_0__ arg_1__ arg_2__ arg_3__ =>
    match arg_0__, arg_1__, arg_2__, arg_3__ with
    | var, fv_cand, in_scope, (pair have haveSet as acc) =>
        if Core.elemVarSet var in_scope : bool then acc else
        if Core.elemVarSet var haveSet : bool then acc else
        if fv_cand var : bool
        then pair (cons var have) (Core.extendVarSet haveSet var) else
        acc
    end.

Definition unionFV : FV -> FV -> FV :=
  fun fv1 fv2 fv_cand in_scope acc =>
    fv1 fv_cand in_scope (fv2 fv_cand in_scope acc).

Definition mapUnionFV {a} : (a -> FV) -> list a -> FV :=
  fix mapUnionFV arg_0__ arg_1__ arg_2__ arg_3__ arg_4__
        := match arg_0__, arg_1__, arg_2__, arg_3__, arg_4__ with
           | _f, nil, _fv_cand, _in_scope, acc => acc
           | f, cons a as_, fv_cand, in_scope, acc =>
               mapUnionFV f as_ fv_cand in_scope (f a fv_cand in_scope acc)
           end.

Definition mkFVs : list Core.Var -> FV :=
  fun vars fv_cand in_scope acc => mapUnionFV unitFV vars fv_cand in_scope acc.

Definition unionsFV : list FV -> FV :=
  fun fvs fv_cand in_scope acc => mapUnionFV GHC.Base.id fvs fv_cand in_scope acc.

Definition fvVarListVarSet : FV -> (list Core.Var * Core.VarSet)%type :=
  fun fv => fv (GHC.Base.const true) Core.emptyVarSet (pair nil Core.emptyVarSet).

Definition fvVarSet : FV -> Core.VarSet :=
  Data.Tuple.snd GHC.Base.∘ fvVarListVarSet.

Definition fvVarList : FV -> list Core.Var :=
  Data.Tuple.fst GHC.Base.∘ fvVarListVarSet.

Definition fvDVarSet : FV -> Core.DVarSet :=
  Core.mkDVarSet GHC.Base.∘ (Data.Tuple.fst GHC.Base.∘ fvVarListVarSet).

Definition filterFV : InterestingVarFun -> FV -> FV :=
  fun fv_cand2 fv fv_cand1 in_scope acc =>
    fv (fun v => andb (fv_cand1 v) (fv_cand2 v)) in_scope acc.

Definition emptyFV : FV :=
  fun arg_0__ arg_1__ arg_2__ =>
    match arg_0__, arg_1__, arg_2__ with
    | _, _, acc => acc
    end.

Definition delFVs : Core.VarSet -> FV -> FV :=
  fun vars fv fv_cand in_scope acc =>
    fv fv_cand (Core.unionVarSet in_scope vars) acc.

Definition delFV : Core.Var -> FV -> FV :=
  fun var fv fv_cand in_scope acc =>
    fv fv_cand (Core.extendVarSet in_scope var) acc.

(* External variables:
     andb bool cons list nil op_zt__ pair true Core.DVarSet Core.Id Core.Var
     Core.VarSet Core.elemVarSet Core.emptyVarSet Core.extendVarSet Core.mkDVarSet
     Core.unionVarSet Data.Tuple.fst Data.Tuple.snd GHC.Base.const GHC.Base.id
     GHC.Base.op_z2218U__
*)

author: DavidFHCh

repo: Tesis-FTW

save_path: github-repos/coq/DavidFHCh-Tesis-FTW


text:
Require Import Category.Lib.
Require Import Category.Theory.Category.
Require Import Category.Theory.Isomorphism.
Require Import Category.Theory.Functor.
Require Import Category.Theory.Natural.Transformation.
Require Import Category.Instance.Sets.

Generalizable All Variables.

Section Fun.

Context {C : Category}.
Context {D : Category}.

(* Fun is the category whose morphisms are natural transformations between
   Functors from C ⟶ D. *)

Program Definition Fun : Category := {|
  obj     := C ⟶ D;
  hom     := @Transform C D;
  id      := @nat_id C D;
  compose := @nat_compose C D;

  compose_respects := @nat_compose_respects C D
|}.

End Fun.

Notation "[ C , D ]" := (@Fun C D)
  (at level 90, right associativity, format "[ C ,  D ]") : category_scope.

Notation "[[[ C , D ]]]( F , G )" := ({| carrier   := @hom (@Fun C D) F G
                                       ; is_setoid := @homset (@Fun C D) F G |})
  (at level 90, right associativity, format "[[[ C ,  D ]]]( F , G )") : homset_scope.

Corollary nat_id_left C D (F G : C ⟶ D) (N : F ⟹ G) :
  nat_id ∙ N ≈[Fun] N.
Proof. unfold nat_id, nat_compose; simpl; intros; cat. Qed.

Corollary nat_id_right C D (F G : C ⟶ D) (N : F ⟹ G) :
  N ∙ nat_id ≈[Fun] N.
Proof. unfold nat_id, nat_compose; simpl; intros; cat. Qed.

Corollary nat_comp_assoc C D (F G H J : C ⟶ D)
          (M : H ⟹ J) (N : G ⟹ H) (O : F ⟹ G) :
  M ∙ (N ∙ O) ≈[Fun] (M ∙ N) ∙ O.
Proof. unfold nat_compose; simpl; intros; cat. Qed.

Lemma whisker_right_id A B C (F : A ⟶ B) (G : B ⟶ C) : id{Fun} ⊲ F ≈ id{Fun}.
Proof. simpl; intros; cat. Qed.

Lemma whisker_left_id A B C (F : A ⟶ B) (G : B ⟶ C) : G ⊳ id{Fun} ≈ id{Fun}.
Proof. simpl; intros; cat. Qed.

Lemma whisker_left_dist A B C (F : A ⟶ B) (G H J : B ⟶ C)
      (η : G ⟹ H) (θ : H ⟹ J) : (θ ⊲ F) ∙ (η ⊲ F) ≈ (θ ∙ η) ⊲ F.
Proof. simpl; intros; cat. Qed.

Lemma whisker_right_dist A B C (F G H : A ⟶ B) (J : B ⟶ C)
      (η : F ⟹ G) (θ : G ⟹ H) : (J ⊳ θ) ∙ (J ⊳ η) ≈ J ⊳ (θ ∙ η).
Proof. simpl; intros; cat. now rewrite fmap_comp. Qed.

Definition nat_λ {A B} (F : A ⟶ B) : F ◯ Id ≅[Fun] F.
Proof.
  construct.
  - apply fun_id_right.
  - apply fun_id_right_sym.
  - apply fun_id_right_and_sym.
  - apply fun_id_right_sym_and.
Defined.

Definition nat_ρ {A B} (F : A ⟶ B) : Id ◯ F ≅[Fun] F.
Proof.
  construct.
  - apply fun_id_left.
  - apply fun_id_left_sym.
  - apply fun_id_left_and_sym.
  - apply fun_id_left_sym_and.
Defined.

Definition nat_α {A B C D} (F : A ⟶ B) (G : B ⟶ C) (H : C ⟶ D) :
  H ◯ (G ◯ F) ≅[Fun] (H ◯ G) ◯ F.
Proof.
  construct.
  - apply fun_comp_assoc.
  - apply fun_comp_assoc_sym.
  - apply fun_comp_assoc_and_sym.
  - apply fun_comp_assoc_sym_and.
Defined.

Lemma whisker_left_right A B C (F G : A ⟶ B) (H J : B ⟶ C)
      (η : F ⟹ G) (θ : H ⟹ J) :
  (J ⊳ η) ∙ (θ ⊲ F) ≈ (θ ⊲ G) ∙ (H ⊳ η).
Proof. simpl; intros; cat; apply naturality. Qed.

Lemma whisker_flip A B C (F : A ⟶ B) (G : B ⟶ C) :
  (to (nat_λ G) ⊲ F) ∙ to (nat_α F Id G) ≈ G ⊳ (to (nat_ρ F)).
Proof. simpl; intros; cat. Qed.

Lemma nat_α_whisker_right_comp
      A B C D (F : A ⟶ B) (G : B ⟶ C) (H J : C ⟶ D) (η : H ⟹ J) :
  to (nat_α F G J) ∙ η ⊲ (G ◯ F) ≈ (η ⊲ G) ⊲ F ∙ to (nat_α F G H).
Proof. simpl; intros; cat. Qed.

Lemma nat_α_whisker_left_comp
      A B C D (F G : A ⟶ B) (H : B ⟶ C) (J : C ⟶ D) (η : F ⟹ G) :
  to (nat_α G H J) ∙ J ⊳ (H ⊳ η) ≈ (J ◯ H) ⊳ η ∙ to (nat_α F H J).
Proof. simpl; intros; cat. Qed.

Lemma nat_α_whisker_assoc
      A B C D (F : A ⟶ B) (G H : B ⟶ C) (J : C ⟶ D) (η : G ⟹ H) :
  to (nat_α F H J) ∙ J ⊳ (η ⊲ F) ≈ (J ⊳ η) ⊲ F ∙ to (nat_α F G J).
Proof. simpl; intros; cat. Qed.

Lemma nat_α_nat_α A B C D E (F : A ⟶ B) (G : B ⟶ C) (H : C ⟶ D) (J : D ⟶ E) :
  (to (nat_α G H J) ⊲ F ∙ to (nat_α F (H ◯ G) J)) ∙ (J ⊳ (to (nat_α F G H)))
    ≈ to (nat_α F G (J ◯ H)) ∙ to (nat_α (G ◯ F) H J).
Proof. simpl; intros; cat. Qed.

Class Pointed {C : Category} (F : C ⟶ C) := {
  point : Id ⟹ F
}.

Class WellPointed `{@Pointed C F} := {
  well_pointed :
    (F ⊳ point) ∙ from (nat_λ _) ≈ (point ⊲ F) ∙ from (nat_ρ _)
}.

Theorem Functor_Setoid_Nat_Iso `(F : C ⟶ D) (G : C ⟶ D) :
  F ≅[Fun] G  ↔  F ≈ G.
Proof.
  split; intros; simpl.
  - given (iso : ∀ x : C, F x ≅ G x). {
      intros; isomorphism; simpl; intros.
      - apply X.
      - apply (X⁻¹).
      - abstract (srewrite (iso_to_from X); cat).
      - abstract (srewrite (iso_from_to X); cat).
    }
    exists iso; simpl in *; intros.
    abstract
      (rewrite <- comp_assoc;
       rewrite (naturality[to X]);
       rewrite comp_assoc;
       srewrite (iso_from_to X); cat).
  - destruct X.
    isomorphism; simpl; intros.
    + transform; simpl; intros.
      * apply x.
      * abstract
          (rewrite e; simpl;
           rewrite !comp_assoc;
           rewrite iso_to_from; cat).
      * abstract
          (rewrite e; simpl;
           rewrite !comp_assoc;
           rewrite iso_to_from; cat).
    + transform; simpl; intros.
      * apply x.
      * abstract
          (rewrite e; simpl;
           rewrite <- !comp_assoc;
           rewrite iso_to_from; cat).
      * abstract
          (rewrite e; simpl;
           rewrite <- !comp_assoc;
           rewrite iso_to_from; cat).
    + abstract
        (rewrite fmap_id;
         apply iso_to_from).
    + abstract
        (rewrite fmap_id;
         apply iso_from_to).
Defined.

Definition iso_equiv {C D : Category} {f g : C ⟶ D} :
  f ≅[Fun] g → f ≈ g := fst (Functor_Setoid_Nat_Iso _ _).

Definition equiv_iso {C D : Category} {f g : C ⟶ D} :
  f ≈ g → f ≅[Fun] g := snd (Functor_Setoid_Nat_Iso _ _).

author: jwiegley

repo: category-theory


text:
(*

  The definition of First-Oder Logic used here is adapted from
  the following library: https://github.com/uds-psl/coq-library-undecidability/

*)

Require Import Vector List Lia.

Require Import Coq.Vectors.Vector.
Definition vec := t.

Require Import Equations.Equations.

(* Some preliminary definitions for substitions  *)
Definition scons {X: Type} (x : X) (xi : nat -> X) :=
  fun n => match n with
        | 0 => x
        | S n => xi n
        end.

Definition funcomp {X Y Z} (g : Y -> Z) (f : X -> Y)  :=
  fun x => g (f x).

(* Signatures are a record to allow for easier definitions of general transformations on signatures *)

Class funcs_signature :=
  { syms : Type; ar_syms : syms -> nat }.

Coercion syms : funcs_signature >-> Sortclass.

Class preds_signature :=
  { preds : Type; ar_preds : preds -> nat }.

Coercion preds : preds_signature >-> Sortclass.

Section fix_signature.

  Context {Σ_funcs : funcs_signature}.

  Unset Elimination Schemes.

  Inductive term  : Type :=
  | var : nat -> term
  | func : forall (f : syms), vec term (ar_syms f) -> term.

  Set Elimination Schemes.

  Fixpoint subst_term (σ : nat -> term) (t : term) : term :=
    match t with
    | var t => σ t
    | func f v => func f (map (subst_term σ) v)
    end.

  Context {Σ_preds : preds_signature}.

  (* Syntax is parametrised in binary operators and quantifiers. *)
  Class operators := {binop : Type ; quantop : Type}.
  Context {ops : operators}.

  (* Formulas have falsity as fixed constant *)
  Inductive form : Type :=
  | atom : forall (P : preds), vec term (ar_preds P) -> form
  | bin : binop -> form -> form -> form
  | quant : quantop -> form -> form.

  Definition up (σ : nat -> term) := scons (var 0) (funcomp (subst_term (funcomp var S)) σ).

  Fixpoint subst_form (σ : nat -> term) (phi : form) : form :=
    match phi with
    | atom P v => atom P (map (subst_term σ) v)
    | bin op phi1 phi2 => bin op (subst_form σ phi1) (subst_form σ phi2)
    | quant op phi => quant op (subst_form (up σ) phi)
    end.

  Fixpoint depth_form (phi : form) : nat :=
      match phi with
      | atom P v => 0
      | bin op phi1 phi2 => S(depth_form phi1 + depth_form phi2)
      | quant op phi => S (depth_form phi)
      end.

End fix_signature.

Arguments term _, {_}.
Arguments var _ _, {_} _.
Arguments func _ _ _, {_} _ _.
Arguments subst_term {_} _ _.

Arguments form  _ _ _, _ _ {_}, {_ _ _}.
Arguments atom  _ _ _ _, _ _ {_ _}, {_ _ _ _}.
Arguments bin   _ _ _ _, _ _ {_ _}, {_ _ _ _}.
Arguments quant _ _ _ _, _ _ {_ _}, {_ _ _ _}.

Arguments up         _, {_}.
Arguments subst_form _ _ _, _ _ {_}, {_ _ _}.

(* Substitution Notation *)

Declare Scope subst_scope.
Open Scope subst_scope.

Notation "$ x" := (var x) (at level 3, format "$ '/' x") : subst_scope.
Notation "t `[ sigma ]" := (subst_term sigma t) (at level 7, left associativity, format "t '/' `[ sigma ]") : subst_scope.
Notation "phi [ sigma ]" := (subst_form sigma phi) (at level 7, left associativity, format "phi '/' [ sigma ]") : subst_scope.
Notation "s .: sigma" := (scons s sigma) (at level 70, right associativity) : subst_scope.
Notation "f >> g" := (funcomp g f) (at level 50) : subst_scope.
Notation "s '..'" := (scons s var) (at level 4, format "s ..") : subst_scope.
Notation "↑" := (S >> var) : subst_scope.

(* * Full Syntax *)

Declare Scope syn.
Open Scope syn.

Inductive full_logic_sym : Type :=
| Conj : full_logic_sym
| Disj : full_logic_sym
| Impl : full_logic_sym.

Inductive full_logic_quant : Type :=
| All : full_logic_quant
| Ex : full_logic_quant.

Definition full_operators : operators :=
  {| binop := full_logic_sym ; quantop := full_logic_quant |}.

#[export] Hint Immediate full_operators : typeclass_instances.

Notation "∀ Phi" := (@quant _ _ full_operators All Phi) (at level 50) : syn.
Notation "∃ Phi" := (@quant _ _ full_operators Ex Phi) (at level 50) : syn.
Notation "A ∧ B" := (@bin _ _ full_operators Conj A B) (at level 41) : syn.
Notation "A ∨ B" := (@bin _ _ full_operators Disj A B) (at level 42) : syn.
Notation "A '-->' B" := (@bin _ _ full_operators Impl A B) (at level 43, right associativity) : syn.
Notation "A '<-->' B" := ((A --> B) ∧ (B --> A)) (at level 43) : syn.

Require Import List.

Notation "x 'el' A" := (In x A) (at level 70).
Notation "A '<<=' B" := (incl A B) (at level 70).

Local Set Implicit Arguments.

Section ND_def.

  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.

  Reserved Notation "A ⊢ phi" (at level 61).

  (* Definition of natural deduction for minimal logic *)

  Inductive prv : list form -> form -> Type :=
  | II A phi psi : phi::A ⊢ psi -> A ⊢ (phi --> psi)
  | IE A phi psi : A ⊢ phi --> psi -> A ⊢ phi -> A ⊢ psi
  | AllI A phi : map (subst_form ↑) A ⊢ phi -> A ⊢ ∀ phi
  | AllE A t phi : A ⊢ ∀ phi -> A ⊢ phi[t..]
  | ExI A t phi : A ⊢ phi[t..] -> A ⊢ ∃ phi
  | ExE A phi psi : A ⊢ ∃ phi -> phi::(map (subst_form ↑) A) ⊢ psi[↑] -> A ⊢ psi
  | Ctx A phi : phi el A -> A ⊢ phi
  | CI A phi psi : A ⊢ phi -> A ⊢ psi -> A ⊢ phi ∧ psi
  | CE1 A phi psi : A ⊢ phi ∧ psi -> A ⊢ phi
  | CE2 A phi psi : A ⊢ phi ∧ psi -> A ⊢ psi
  | DI1 A phi psi : A ⊢ phi -> A ⊢ phi ∨ psi
  | DI2 A phi psi : A ⊢ psi -> A ⊢ phi ∨ psi
  | DE A phi psi theta : A ⊢ phi ∨ psi -> phi::A ⊢ theta -> psi::A ⊢ theta -> A ⊢ theta
  where "A ⊢ phi" := (prv A phi).

End ND_def.

Arguments prv {_ _} _ _.
Notation "A ⊢M phi" := (prv A phi) (at level 55).

Section Minimal.

  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.

(*  We formulate stability and explosiveness with respect to some fixed
    closed formula ⊥ of our minimal logic. We can then show that if all
    atomic formulas are explosive with respect to ⊥, then all formulas
    are explosive with respect to ⊥.
*)
  Variable falsity : form.
  Notation "⊥" := (falsity).
  Notation "¬ A" := (A --> ⊥) (at level 42) : syn.
  Hypothesis closed_bot : forall σ, ⊥[σ] = ⊥.

  (* Stability and Explosiveness with respect to ⊥ *)
  Definition stable ϕ := forall Γ, Γ ⊢M (((ϕ --> ⊥) --> ⊥) --> ϕ).
  Definition explosive ϕ := forall Γ, Γ ⊢M (⊥ --> ϕ).
  Definition stable_atoms := forall P t, stable (@atom _ _ _ P t).
  Definition explosive_atoms := forall P t, explosive (@atom _ _ _ P t).

  Fact stable_explosive ϕ :
    stable ϕ -> explosive ϕ.
  Proof.
    intros H Γ. apply II.
    eapply IE. apply H.
    apply II, Ctx; firstorder.
  Qed.

  Fact bot_el {ϕ Γ} :
    explosive ϕ -> ⊥ el Γ -> Γ ⊢M ϕ.
  Proof.
    intros Exp El.
    eapply IE with ⊥; [apply Exp| now apply Ctx].
  Qed.

  Lemma size_rect {X} σ f :
    (forall x, (forall y : X, σ y < σ x -> f y) -> f x) -> forall x, f x.
  Proof.
    intros H x. apply H.
    induction (σ x).
    - intros y. now intros F % PeanoNat.Nat.nlt_0_r.
    - intros y Hy. apply H.
      intros z Hz. apply IHn. lia.
  Defined.

  Fact depth_invar phi :
    forall sigma, depth_form(phi[sigma]) = depth_form phi.
  Proof.
    induction phi; cbn; congruence.
  Qed.

  Lemma Explosion :
    explosive_atoms -> forall ϕ, explosive ϕ.
  Proof.
    intros exp phi.
    pattern phi; revert phi.
    apply (size_rect depth_form).
    intros [| b phi1 phi2 | q phi ] Rec Γ; apply II.
    - apply bot_el; cbn; auto.
    - destruct b.
      + unshelve refine (
          let H := _ : _ in
          let sym phi e := H phi (Rec phi e) in
            CI (sym phi1 _) (sym phi2 _)
        ).
        2,3 : cbn; lia.
        intros A HA.
        refine (bot_el HA _); cbn; auto.
      + apply DI1.
        refine (bot_el (Rec _ _) _); cbn;[lia|auto].
      + apply II.
        refine (bot_el (Rec _ _) _); cbn;[lia|auto].
    - destruct q.
      + apply AllI.
        refine (bot_el (Rec _ _) _); cbn;[lia|auto].
      + eapply ExI with (t:= $0).
        refine (bot_el (Rec _ _) _); cbn;[|auto].
        rewrite depth_invar. lia.
  Qed.

  Lemma Explosion' :
    explosive_atoms -> forall ψ ϕ Γ, Γ ⊢M (¬ ψ --> ψ --> ϕ).
  Proof.
    intros exp psi phi Γ. apply II, II.
    eapply IE with ⊥. apply (Explosion exp).
    eapply IE with psi; apply Ctx; firstorder.
  Qed.

  Lemma drinker P x :
  let P_x := @atom _ _ _ P x in
    stable_atoms -> nil ⊢M ¬ ∀ ¬ (P_x --> ∀ P_x).
  Proof.
    cbn. intros stab.
    remember (atom x) as ϕ.
    apply II. eapply IE with ((ϕ --> ∀ ϕ)[$0..]).
    assert (
      (∀ ¬ (ϕ --> (∀ ϕ)) :: Datatypes.nil) ⊢M (¬ (ϕ --> (∀ ϕ)))[$0..]
    ) as H.
    - apply AllE, Ctx; now left.
    - admit.
    - cbn; apply II. apply AllI. cbn.
      subst. eapply IE. cbn.
  Admitted.

  Definition Perice_Transform phi := (⊥ --> phi) --> ⊥.
  Fixpoint PT (phi : form) :=
    match phi with
      | atom _ _ v => Perice_Transform (atom _ _ v)
      | bin _ _ _ Conj phi1 phi2 => (PT phi1) ∧ (PT phi2)
      | bin _ _ _ Disj phi1 phi2 => phi1 ∨ phi2
      | bin _ _ _ Impl phi1 phi2 => (PT phi1) --> (PT phi2)
      | quant _ _ _ Ex phi => ∃ phi
      | quant _ _ _ All phi => ∀ (PT phi)
      end.

  Variable PT_bot : PT ⊥ = ⊥.

  Lemma conservative Gamma phi :
    Gamma ⊢M phi --> PT phi.
  Proof.
    induction phi; cbn; unfold Perice_Transform.
    - apply II, II.
  Admitted.

  Lemma idempotent Gamma ϕ :
    Gamma ⊢M PT (PT ϕ) --> PT ϕ.
  Proof.
    induction ϕ; cbn; unfold Perice_Transform.
    - apply II, II. rewrite PT_bot.
      eapply IE. apply Ctx; firstorder.
      apply II, II. apply Ctx; firstorder.
    - destruct b; cbn.
      + apply II. admit.
      + apply II, Ctx; firstorder.
      +
  Admitted.

End Minimal.

author: HermesMarc


text:
Require Import
  Pact.Lib
  Pact.Ty
  Pact.Exp
  Pact.Value
  Pact.Walk
  Pact.Ren.

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

Set Equations With UIP.

Generalizable All Variables.
Set Primitive Projections.

Import ListNotations.

Inductive Sub (Γ : Env) : Env → Set :=
  | NoSub : Sub Γ []
  | Push {Γ' τ} : Exp Γ τ → Sub Γ Γ' → Sub Γ (τ :: Γ').

#[global] Arguments NoSub {Γ}.
#[global] Arguments Push {Γ Γ' τ} _ _.

Derive Signature NoConfusion NoConfusionHom Subterm for Sub.

Equations get `(s : Sub Γ' Γ) `(v : Var Γ τ) : Exp Γ' τ :=
  get (Push x _)   ZV    := x;
  get (Push _ xs) (SV v) := get xs v.

Equations ScR {Γ Γ' Γ''} (s : Sub Γ' Γ'') (r : Ren Γ Γ') : Sub Γ Γ'' :=
  ScR NoSub      δ := NoSub;
  ScR (Push t σ) δ := Push (RenExp δ t) (ScR σ δ).

Lemma ScR_idRen {Γ Γ'} (s : Sub Γ Γ') :
  ScR s idRen = s.
Proof.
  induction s; simp ScR;
  rewrite ?RenExp_idRen; sauto.
Qed.

Fixpoint idSub {Γ} : Sub Γ Γ :=
  match Γ with
  | []     => NoSub
  | τ :: Γ => Push (VAR ZV) (ScR (@idSub Γ) skip1)
  end.

Corollary NoSub_idSub : NoSub (Γ:=[]) = idSub.
Proof. reflexivity. Qed.

Equations RcS {Γ Γ' Γ''} (r : Ren Γ' Γ'') (s : Sub Γ Γ') : Sub Γ Γ'' :=
  RcS NoRen    δ          := δ;
  RcS (Drop σ) (Push t δ) := RcS σ δ;
  RcS (Keep σ) (Push t δ) := Push t (RcS σ δ).

Definition Dropₛ {Γ Γ' τ} (s : Sub Γ Γ') : Sub (τ :: Γ) Γ' :=
  ScR s skip1.

Definition Keepₛ {Γ Γ' τ} (s : Sub Γ Γ') : Sub (τ :: Γ) (τ :: Γ') :=
  Push (VAR ZV) (Dropₛ s).

Corollary Keepₛ_idSub {Γ τ} :
  Keepₛ (Γ:=Γ) (Γ':=Γ) (τ:=τ) idSub = idSub.
Proof. reflexivity. Qed.

Equations SubVar {Γ Γ' τ} (s : Sub Γ Γ') (v : Var Γ' τ) : Exp Γ τ :=
  SubVar (Push t σ) ZV     := t;
  SubVar (Push t σ) (SV v) := SubVar σ v.

Definition SubExp {Γ Γ' τ} (s : Sub Γ Γ') (e : Exp Γ' τ) : Exp Γ τ :=
  WalkExp s (@Keepₛ) (λ _ _ _ r v, SubVar r v) e.

Lemma SubVar_ScR {Γ Γ' Γ'' τ} (σ : Sub Γ' Γ'') (δ : Ren Γ Γ') (v : Var Γ'' τ) :
  SubVar (ScR σ δ) v = RenExp δ (SubVar σ v).
Proof.
  induction σ; simp SubVar; simp ScR.
  - sauto.
  - now dependent elimination v; simp SubVar.
Qed.

Lemma SubVar_idSub {Γ τ} (v : Var Γ τ) :
  SubVar idSub v = VAR v.
Proof.
  induction v; simpl; simp SubVar; auto.
  rewrite SubVar_ScR IHv /= RenVar_skip1 //.
Qed.

Lemma SubExp_idSub {Γ τ} (e : Exp Γ τ) :
  SubExp idSub e = e.
Proof.
  induction e; simpl;
  rewrite ?SubVar_idSub; sauto.
Qed.

Lemma ScR_ScR {Γ Γ' Γ'' Γ'''} (σ : Sub Γ'' Γ''') (δ : Ren Γ' Γ'') (ν : Ren Γ Γ') :
  ScR (ScR σ δ) ν = ScR σ (RcR δ ν).
Proof.
  induction σ; simp ScR;
  rewrite ?RenExp_RcR; sauto.
Qed.

Lemma ScR_RcS {Γ Γ' Γ'' Γ'''} (σ : Ren Γ'' Γ''') (δ : Sub Γ' Γ'') (ν : Ren Γ Γ') :
  ScR (RcS σ δ) ν = RcS σ (ScR δ ν).
Proof.
  induction σ;
  dependent elimination δ;
  simp RcS; simp ScR; sauto.
Qed.

Lemma RcS_idRen {Γ Γ'} (σ : Sub Γ Γ') :
  RcS idRen σ = σ.
Proof.
  induction σ; simp RcS; simpl; simp RcS; sauto.
Qed.

Lemma RcS_idSub {Γ Γ'} (σ : Ren Γ Γ') :
  RcS σ idSub = ScR idSub σ.
Proof.
  induction σ; simp RcS; simpl; simp RcS; simp ScR; auto.
  - rewrite -ScR_RcS IHσ ScR_ScR /skip1.
    simp RcR.
    rewrite RcR_idRen_right //.
  - rewrite -ScR_RcS IHσ !ScR_ScR /skip1.
    simp RcR.
    rewrite RcR_idRen_left RcR_idRen_right //.
Qed.

Corollary RcS_skip1 {Γ Γ' τ} (e : Exp Γ τ) (σ : Sub Γ Γ') :
  RcS skip1 (Push e σ) = σ.
Proof.
  rewrite /skip1.
  simp RcS.
  rewrite RcS_idRen //.
Qed.

Lemma RcS_DropAll {Γ Γ'} (σ : Sub Γ' Γ) :
  RcS DropAll σ = NoSub.
Proof.
  now induction σ; simp RcS.
Qed.

Lemma SubVar_RcS {Γ Γ' Γ'' τ} (σ : Ren Γ' Γ'') (δ : Sub Γ Γ') (v : Var Γ'' τ) :
  SubVar (RcS σ δ) v = SubVar δ (RenVar σ v).
Proof.
  induction σ; simp RenVar; auto.
  - dependent elimination δ.
    now simp RcS.
  - dependent elimination δ.
    dependent elimination v;
    now simp RcS; simp RenVar; simp SubVar.
Qed.

Lemma SubExp_RcS {Γ Γ' Γ'' τ} (σ : Ren Γ' Γ'') (δ : Sub Γ Γ') (e : Exp Γ'' τ) :
  SubExp (RcS σ δ) e = SubExp δ (RenExp σ e).
Proof.
  generalize dependent Γ'.
  generalize dependent Γ.
  induction e; simpl; intros; auto.
  1: now rewrite SubVar_RcS.
  1: {
    specialize (IHe _ _ (Keep σ) (Keepₛ δ)).
    rewrite -IHe /Keepₛ /Dropₛ ScR_RcS.
    now simp RcS.
  }
  2: {
    rewrite -IHe1 -IHe2 /Keepₛ /Dropₛ ScR_RcS.
    now simp RcS.
  }
  all: sauto.
Qed.

Lemma SubExp_ScR {Γ Γ' Γ'' τ} (σ : Sub Γ' Γ'') (δ : Ren Γ Γ') (e : Exp Γ'' τ) :
  SubExp (ScR σ δ) e = RenExp δ (SubExp σ e).
Proof.
  generalize dependent Γ'.
  generalize dependent Γ.
  induction e; simpl; intros; auto.
  1: now rewrite SubVar_ScR.
  1: {
    rewrite -IHe /Keepₛ /Dropₛ /= ScR_ScR.
    simp ScR; simpl.
    simp RenVar.
    rewrite ScR_ScR /skip1.
    simp RcR.
    rewrite RcR_idRen_left RcR_idRen_right //.
  }
  2: {
    rewrite -IHe1 -IHe2 /Keepₛ /Dropₛ /= ScR_ScR.
    simp ScR; simpl.
    simp RenVar.
    rewrite ScR_ScR /skip1.
    simp RcR.
    rewrite RcR_idRen_left RcR_idRen_right //.
  }
  all: sauto.
Qed.

Fixpoint ScS {Γ Γ' Γ''} (s : Sub Γ' Γ'') (δ : Sub Γ Γ') : Sub Γ Γ'' :=
  match s with
  | NoSub    => NoSub
  | Push e σ => Push (SubExp δ e) (ScS σ δ)
  end.

Lemma ScS_ScR {Γ Γ' Γ'' Γ'''} (σ : Sub Γ'' Γ''') (δ : Ren Γ' Γ'') (ν : Sub Γ Γ') :
  ScS (ScR σ δ) ν = ScS σ (RcS δ ν).
Proof.
  generalize dependent Γ'.
  generalize dependent Γ.
  induction σ; simp ScR; simp ScS;
  simpl; intros; auto; simp ScR.
  rewrite /= -SubExp_RcS; sauto.
Qed.

Lemma ScR_ScS {Γ Γ' Γ'' Γ'''} (σ : Sub Γ'' Γ''') (δ : Sub Γ' Γ'') (ν : Ren Γ Γ') :
  ScR (ScS σ δ) ν = ScS σ (ScR δ ν).
Proof.
  generalize dependent Γ'.
  generalize dependent Γ.
  induction σ; simp ScR; simp ScS;
  simpl; intros; auto; simp ScR.
  rewrite /= -SubExp_ScR; sauto.
Qed.

Lemma SubVar_ScS {Γ Γ' Γ'' τ} (σ : Sub Γ' Γ'') (δ : Sub Γ Γ') (v : Var Γ'' τ) :
  SubVar (ScS σ δ) v = SubExp δ (SubVar σ v).
Proof.
  induction σ; simp SubVar; simp ScR.
  - sauto.
  - now dependent elimination v; simpl; simp SubVar.
Qed.

Lemma SubExp_ScS {Γ Γ' Γ'' τ} (σ : Sub Γ' Γ'') (δ : Sub Γ Γ') (e : Exp Γ'' τ) :
  SubExp (ScS σ δ) e = SubExp δ (SubExp σ e).
Proof.
  generalize dependent Γ'.
  generalize dependent Γ.
  induction e; simpl; intros; auto.
  1: now rewrite SubVar_ScS.
  1: {
    rewrite -IHe /Keepₛ /Dropₛ /= ScR_ScS.
    simp SubVar.
    remember (ScR δ skip1) as g.
    unfold skip1.
    generalize dependent g.
    generalize dependent Γ0.
    destruct σ; simpl; simp ScR;
    simpl; intros; auto.
    rewrite -SubExp_RcS.
    simp RcS.
    rewrite RcS_idRen ScS_ScR.
    simp RcS.
    now rewrite RcS_idRen.
  }
  2: {
    rewrite -IHe1 -IHe2 /Keepₛ /Dropₛ /= ScR_ScS.
    simp SubVar.
    remember (ScR δ skip1) as g.
    unfold skip1.
    generalize dependent g.
    generalize dependent Γ0.
    destruct σ; simpl; simp ScR;
    simpl; intros; auto.
    rewrite -SubExp_RcS.
    simp RcS.
    rewrite RcS_idRen ScS_ScR.
    simp RcS.
    now rewrite RcS_idRen.
  }
  all: sauto.
Qed.

Lemma ScS_idSub_right {Γ Γ'} (σ : Sub Γ Γ') :
  ScS σ idSub = σ.
Proof.
  induction σ; simpl; rewrite ?SubExp_idSub; sauto.
Qed.

Lemma ScS_idSub_left {Γ Γ'} (σ : Sub Γ Γ') :
  ScS idSub σ = σ.
Proof.
  induction σ; rewrite //= ScS_ScR RcS_skip1 IHσ //.
Qed.

Lemma ScS_assoc {Γ Γ' Γ'' Γ'''}
      (σ : Sub Γ'' Γ''') (δ : Sub Γ' Γ'') (ν : Sub Γ Γ') :
  ScS (ScS σ δ) ν = ScS σ (ScS δ ν).
Proof.
  induction σ; simpl; auto.
  rewrite -SubExp_ScS /=.
  now f_equal.
Qed.

Lemma ScS_Keepₛ {Γ Γ' Γ'' τ} (f : Sub Γ' Γ'') (g : Sub Γ Γ') :
  ScS (Keepₛ (τ:=τ) f) (Keepₛ g) = Keepₛ (ScS f g).
Proof.
  unfold Keepₛ, Dropₛ.
  rewrite /= ScS_ScR ScR_ScS RcS_skip1 //.
Qed.

Notation "{|| e ; .. ; f ||}" := (Push e%exp .. (Push f%exp idSub) ..).

Lemma SubExp_Push {Γ Γ' τ ty} (x : Exp Γ' ty) (s : Sub Γ' Γ) (e : Exp (ty :: Γ) τ) :
  SubExp (Push x s) e = SubExp {|| x ||} (SubExp (Keepₛ s) e).
Proof.
  rewrite -SubExp_ScS /= ScS_ScR RcS_skip1 ScS_idSub_right //.
Qed.

Corollary SubExp_closed `(s : Sub [] []) `(e : [] ⊢ τ) :
  SubExp s e = e.
Proof.
  dependent elimination s.
  rewrite NoSub_idSub SubExp_idSub //.
Qed.

Lemma SubExp_SubExp `(s : Sub [] Γ) (s' : Sub Γ []) `(e : [] ⊢ τ) :
  SubExp s (SubExp s' e) = e.
Proof.
  simpl; induction s; dependent elimination s'.
  - rewrite NoSub_idSub !SubExp_idSub //.
  - rewrite -SubExp_ScS /= NoSub_idSub SubExp_idSub //.
Qed.

Lemma SubExp_RenExp `(s : Sub [] Γ) (r' : Ren Γ []) `(e : [] ⊢ τ) :
  SubExp s (RenExp r' e) = e.
Proof.
  simpl; induction s; dependent destruction r'.
  - rewrite NoSub_idSub SubExp_idSub NoRen_idRen RenExp_idRen //.
  - rewrite -SubExp_RcS.
    simp RcS.
    now rewrite SubExp_RcS.
Qed.

Lemma SubExp_ValueP {Γ Γ' τ} {v : Exp Γ τ} (σ : Sub Γ' Γ) :
  ValueP v → ValueP (SubExp σ v).
Proof.
  induction 1; sauto lq: on.
Qed.

(* Substitutions form a category. *)
(*
Definition SubCat : Category := {|
  obj              := Env;
  hom              := Sub;
  homset           := λ _ _, {| Setoid.equiv := eq |};
  Category.id      := @idSub;
  Category.compose := @ScS;
  id_left          := @ScS_idSub_left;
  id_right         := @ScS_idSub_right;
  comp_assoc       := λ _ _ _ _ f g h, eq_sym (ScS_assoc f g h);
  comp_assoc_sym   := @ScS_assoc
|}.
*)

author: kadena-io

repo: pact-model

save_path: github-repos/coq/kadena-io-pact-model


text:
(* monae: Monadic equational reasoning in Coq                                 *)
(* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
From mathcomp Require Import all_ssreflect.
From HB Require Import structures.
Require Import monae_lib hierarchy monad_lib.

(******************************************************************************)
(*                          Composing monads                                  *)
(*                                                                            *)
(* formalization of [Jones and Duponcheel, Composing Monads, Yale RR 1993]    *)
(* (Sections 2 and 3)                                                         *)
(*                                                                            *)
(******************************************************************************)

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

Local Open Scope monae_scope.

Section comp.
Variables (M N : monad).
Definition ret_comp : FId ~~> [the functor of M \o N] := (@ret M) \h (@ret N).
Lemma naturality_ret : naturality FId [the functor of M \o N] ret_comp.
Proof. by move=> A B h; rewrite -(natural ((@ret M) \h (@ret N))). Qed.
HB.instance Definition _ := isNatural.Build
  FId [the functor of (M \o N)] ret_comp naturality_ret.
End comp.
Definition CRet (M N : monad) := [the FId ~> [the functor of M \o N] of ret_comp M N].

Module Prod.
Section prod.
Variables M N(* NB: actually, premonad is enough for N*) : monad.
Variable prod : N \o (M \o N) ~~> M \o N.
Arguments prod {_}.

Definition JOIN : (M \o N) \o (M \o N) ~~> M \o N := fun _ => Join \o M # prod.
Arguments JOIN {_}.

Definition prod1 := forall (A B : UU0) (f : A -> B), prod \o N # ([the functor of M \o N] # f) = [the functor of M \o N] # f \o prod.
Definition prod2 := forall A, prod \o Ret = id :> (_ -> (M \o N) A).
Definition prod3 := forall A, prod \o N # CRet M N _ = Ret :> (_ -> (M \o N) A).
Definition prod4 := forall A, prod \o N # JOIN = JOIN \o prod :> (_ -> (M \o N) A).
Hypothesis Hprod1 : prod1.
Hypothesis Hprod2 : prod2.
Hypothesis Hprod3 : prod3.
Hypothesis Hprod4 : prod4.

Lemma JOIN_naturality : naturality _ _ (@JOIN).
Proof.
move=> A B g; apply/esym; rewrite {1}/JOIN -[in LHS]compA.
transitivity (
  Join \o (M # prod \o M # ([the functor of N \o (M \o N)] # g))).
  by [].
rewrite -functor_o Hprod1.
rewrite functor_o [LHS]compA /JOIN FCompE -(FCompE M M).
rewrite -(natural join).
by rewrite -compA.
Qed.

HB.instance Definition _ := isNatural.Build
  [the functor of (M \o N) \o (M \o N)] [the functor of M \o N] (@JOIN) JOIN_naturality.

Definition JOIN' : [the functor of (M \o N) \o (M \o N)] ~> [the functor of M \o N] :=
  [the _ ~> _ of @JOIN].

Lemma JOIN_ret : JoinLaws.left_unit (CRet M N) (@JOIN').
Proof.
move=> A; rewrite /JOIN'.
rewrite /=.
rewrite /CRet.
rewrite compA.
rewrite -(compA Join (M # prod) Ret) (natural ret).
by rewrite [LHS]compA (compA Join) joinretM compidf Hprod2.
Qed.

Lemma JOIN_fmap_ret : JoinLaws.right_unit (@CRet M N) (@JOIN').
Proof.
move=> A.
rewrite /JOIN' /=.
rewrite -compA.
rewrite FCompE.
rewrite -(@functor_o M).
by rewrite Hprod3 joinMret.
Qed.

Lemma JOIN_fmap_JOIN : JoinLaws.associativity (@JOIN').
Proof.
move=> A; rewrite {1 2}/JOIN' -[LHS]compA /=.
rewrite -functor_o.
rewrite Hprod4.
rewrite {1}/JOIN.
rewrite -(compA Join (M # prod) prod).
rewrite functor_o.
rewrite [LHS]compA.
rewrite joinA.
rewrite -compA.
rewrite functor_o.
rewrite (compA Join (M # (M # prod)) (M # prod)).
by rewrite -(natural _).
Qed.

End prod.
End Prod.

Module Dorp.
Section dorp.
Variables M  (* actually, premonad is enough for M *) N : monad.
Variable dorp : M \o (N \o M) ~~> M \o N.
Arguments dorp {_}.

Definition JOIN : (M \o N) \o (M \o N) ~~> M \o N := fun _ => M # Join \o dorp.
Arguments JOIN {_}.

Definition dorp1 := forall (A B : UU0) (f : A -> B), dorp \o [the functor of M \o N] # (M # f) = [the functor of M \o N] # f \o dorp.
Definition dorp2 := forall A, (@dorp A) \o CRet M N _ = M # Ret.
Definition dorp3 := forall A, (@dorp A) \o [the functor of M \o N] # Ret = id.
Definition dorp4 := forall A, (@dorp A) \o JOIN = JOIN \o [the functor of M \o N] # dorp.
Hypothesis Hdorp1 : dorp1.
Hypothesis Hdorp2 : dorp2.
Hypothesis Hdorp3 : dorp3.
Hypothesis Hdorp4 : dorp4.

Lemma join_naturality : naturality _ _ (@JOIN).
Proof.
move=> A B g; apply/esym; rewrite {1}/JOIN -compA Hdorp1.
rewrite [LHS]compA.
rewrite (FCompE M N (N # g)).
rewrite -(@functor_o M).
rewrite -natural.
by rewrite functor_o.
Qed.

HB.instance Definition _ := isNatural.Build
  [the functor of ((M \o N) \o (M \o N))] [the functor of (M \o N)] (@JOIN) join_naturality.

Definition JOIN' : [the functor of (M \o N) \o (M \o N)] ~> [the functor of M \o N] :=
  [the _ ~> _ of (@JOIN)].

Lemma JOIN_ret : JoinLaws.left_unit (@CRet M N) (@JOIN').
Proof.
move=> A; rewrite /JOIN -[LHS]compA Hdorp2.
rewrite -(@functor_o M).
by rewrite joinretM functor_id.
Qed.

Lemma JOIN_fmap_ret : JoinLaws.right_unit (@CRet M N) (@JOIN').
Proof.
move=> A; rewrite /JOIN /CRet.
rewrite -(compA (M # Join) dorp).
rewrite (@functor_o [the functor of M \o N]).
rewrite (compA dorp) Hdorp3.
rewrite compidf -functor_o.
by rewrite joinMret functor_id.
Qed.

Lemma JOIN_fmap_JOIN : JoinLaws.associativity (@JOIN').
Proof.
move=> A; rewrite {1 2}/JOIN'.
rewrite FCompE.
rewrite (@functor_o N).
rewrite -[LHS]compA.
rewrite functor_o.
rewrite (compA dorp).
rewrite Hdorp1.
rewrite -(compA _ dorp).
rewrite (compA (M # Join)) -functor_o.
rewrite joinA.
rewrite functor_o.
rewrite -[LHS]compA.
rewrite (compA (M # Join) dorp).
rewrite -/JOIN.
rewrite -Hdorp4.
by rewrite [LHS]compA.
Qed.

End dorp.
End Dorp.

Module Swap.
Section swap.
Variables M N : monad.
Variable swap : N \o M ~~> M \o N.
Arguments swap {_}.

Definition JOIN : (M \o N) \o (M \o N) ~~> M \o N :=
  fun A => M # Join \o Join \o M # (@swap (N A)).

Lemma JOINE A : @JOIN A = Join \o M # (M # Join \o swap).
Proof.
rewrite /JOIN.
rewrite natural.
rewrite -(compA Join) FCompE.
by rewrite -(@functor_o M).
Qed.

Let prod A := M # (join A) \o (@swap _).
Arguments prod {A}.
Let dorp A := Join \o M # (@swap A).
Arguments dorp {A}.

Fact JOIN_prod A : @JOIN A = Join \o M # prod.
Proof. by rewrite JOINE. Qed.

Fact JOIN_dorp A : @JOIN A = M # Join \o dorp.
Proof. by rewrite /dorp. Qed.

Definition swap1 := forall (A B : UU0) (f : A -> B), swap \o N # (M # f) = M # (N # f) \o swap .
Definition swap2 := forall A, @swap A \o Ret = M # Ret :> (M A -> (M \o N) A).
Definition swap3 := forall A, @swap A \o N # Ret = Ret :> (N A -> (M \o N) A).
Definition swap4 := forall A, (@prod A) \o N # (@dorp _) = (@dorp _) \o (@prod _).
Hypothesis Hswap1 : swap1.
Hypothesis Hswap2 : swap2.
Hypothesis Hswap3 : swap3.
Hypothesis Hswap4 : swap4.

Lemma prod1 : Prod.prod1 (@prod).
Proof.
move=> A B f; rewrite {1}/prod.
rewrite -[LHS]compA Hswap1 (compA (M # Join)) -functor_o.
by rewrite -natural functor_o -compA.
Qed.

Lemma prod2 : Prod.prod2 (@prod).
Proof.
by move=> A; rewrite /prod -[LHS]compA Hswap2 -(@functor_o M) joinretM functor_id.
Qed.

Lemma prod3 : Prod.prod3 (@prod).
Proof.
move=> A; rewrite /prod /CRet.
rewrite (@functor_o N) (compA (M # Join \o swap)) -(compA (_ # Join)) Hswap3.
by rewrite (natural ret) -[LHS]compA joinMret compfid.
Qed.

Lemma prod4 : Prod.prod4 (@prod).
Proof.
move=> A; rewrite {1}/Prod.JOIN -JOIN_prod JOIN_dorp {1}/prod (@functor_o N).
rewrite (compA (M # Join \o swap)) -(compA (_ # Join)) Hswap1.
rewrite (compA (M # Join)) -functor_o joinA functor_o.
rewrite -[LHS]compA -(compA (_ # Join)) (compA (M # Join) swap) -/prod Hswap4.
by rewrite [LHS]compA /Prod.JOIN -JOIN_prod JOIN_dorp.
Qed.

Lemma dorp1 : Dorp.dorp1 (@dorp).
Proof.
move=> A B g; rewrite {1}/dorp -[LHS]compA.
rewrite -(@functor_o M).
by rewrite Hswap1 functor_o (compA Join) -natural -[LHS]compA.
Qed.

Lemma dorp2 : Dorp.dorp2 (@dorp).
Proof.
move=> A; rewrite /dorp /CRet (compA (Join \o M # swap)) -(compA Join).
by rewrite (natural ret) (compA Join) joinretM compidf Hswap2.
Qed.

Lemma dorp3 : Dorp.dorp3 (@dorp).
Proof.
move=> A; rewrite /dorp -[LHS]compA.
by rewrite -(@functor_o M) Hswap3 joinMret.
Qed.

Lemma dorp4 : Dorp.dorp4 (@dorp).
Proof.
move=> A; rewrite {1}/dorp {1}/Dorp.JOIN -JOIN_dorp JOIN_prod.
rewrite (compA (Join \o M # swap)) -(compA Join).
rewrite (natural join).
rewrite (compA Join Join) -joinA.
rewrite -2![LHS]compA FCompE.
rewrite -(@functor_o M) -(@functor_o M).
rewrite (compA Join (M # swap) prod) -/dorp -Hswap4 functor_o.
by rewrite [LHS]compA -JOINE JOIN_dorp.
Qed.

Lemma JOIN_naturality : @naturality _ _ (JOIN).
Proof. by move=> ?? g; rewrite JOINE -/prod (Prod.JOIN_naturality prod1 g) JOINE. Qed.

HB.instance Definition _ := isNatural.Build
  [the functor of ((M \o N) \o (M \o N))] [the functor of (M \o N)] (@JOIN) JOIN_naturality.

Definition JOIN' : [the functor of (M \o N) \o (M \o N)] ~> [the functor of M \o N] :=
  [the _ ~> _ of (@JOIN)].

Lemma JOIN_ret : JoinLaws.left_unit (@CRet M N) (@JOIN').
Proof.
move=> A.
rewrite [JOIN' _]/=.
rewrite JOINE -/prod.
by rewrite (Prod.JOIN_ret prod1 prod2).
Qed.

Lemma JOIN_fmap_ret : JoinLaws.right_unit (@CRet M N) (@JOIN').
Proof.
move=> A.
rewrite [JOIN' _]/=.
by rewrite JOINE -/prod (Prod.JOIN_fmap_ret prod1 prod3).
Qed.

Lemma JOIN_fmap_JOIN : JoinLaws.associativity (@JOIN').
Proof.
move=> A.
rewrite [JOIN' _]/=.
rewrite [X in _ = _ \o X]/=.
by rewrite !JOINE -!/prod (Prod.JOIN_fmap_JOIN prod1 prod4).
Qed.

End swap.
End Swap.

(* wip *)

Section nattrans_cast_lemmas.
Variables (F G : functor).
Lemma IV : [the functor of idfun \o G] ~> F -> G ~> F.
Proof.
move=> [s [] [GFs]].
apply: (@Nattrans.Pack [the functor of G] F _ (Nattrans.Class (isNatural.Axioms_ _ _ _))).
exact: GFs.
Qed.
Lemma VI : [the functor of G \o idfun] ~> F -> G ~> F.
Proof.
move=> [s [] [GFs]].
apply: (@Nattrans.Pack [the functor of G] F _ (Nattrans.Class (isNatural.Axioms_ _ _ _))).
exact: GFs.
Qed.
Variable K J : functor.
Lemma AV : [the functor of G \o K \o J] ~> F -> [the functor of G \o (K \o J)] ~> F.
Proof.
move=> [s [] [GFs]].
apply: (@Nattrans.Pack [the functor of (G \o (K \o J))] F _
         (Nattrans.Class (isNatural.Axioms_ _ _ _))).
exact: GFs.
Qed.
Lemma AV' : [the functor of G \o (K \o J)] ~> F -> [the functor of G \o K \o J] ~> F.
Proof.
move=> [s [] [GFs]].
apply: (@Nattrans.Pack [the functor of (G \o K \o J)] F _
         (Nattrans.Class (isNatural.Axioms_ _ _ _))).
exact: GFs.
Qed.
Lemma VA : F ~> [the functor of G \o K \o J] -> F ~> [the functor of G \o (K \o J)].
Proof.
move=> [s [] [GFs]].
apply: (@Nattrans.Pack F [the functor of (G \o (K \o J))] _
         (Nattrans.Class (isNatural.Axioms_ _ _ _))).
exact: GFs.
Qed.
Lemma VA' : F ~> [the functor of G \o (K \o J)] -> F ~> [the functor of G \o K \o J].
Proof.
move=> [s [] [GFs]].
apply: (@Nattrans.Pack F [the functor of (G \o K) \o J] _
         (Nattrans.Class (isNatural.Axioms_ _ _ _))).
exact: GFs.
Qed.
End nattrans_cast_lemmas.

Module DistributiveLaw.
Section distributivelaw.
Variables S T : monad.
Record t := mk {
  f : [the functor of S \o T] ~> [the functor of T \o S] ;
  unit1 : IV (f \v (@ret S \h [the _ ~> _ of NId T])) =
          VI ([the _ ~> _ of NId T] \h @ret S) ;
  unit2 : VI (f \v ([the _ ~> _ of NId S] \h @ret T)) =
          IV (@ret T \h [the _ ~> _ of NId S]) ;
  multiplication1 :
    AV (f \v (@join S \h [the _ ~> _ of NId T])) =
    ([the _ ~> _ of NId T] \h @join S) \v
    VA ((f \h [the _ ~> _ of NId S]) \v VA' ([the _ ~> _ of NId S] \h f)) ;
  multiplication2 :
    AV' (f \v ([the _ ~> _ of NId S] \h @join T)) =
    (@join T \h [the _ ~> _ of NId S]) \v
    VA' (([the _ ~> _ of NId T] \h f) \v VA (f \h [the _ ~> _ of NId T]))
}.
End distributivelaw.
End DistributiveLaw.
Coercion DistributiveLaw.f : DistributiveLaw.t >-> nattrans.

(* TODO *)
Definition beck (S T : monad) (f : DistributiveLaw.t S T) : monad.
have @join : [the functor of (T \o S) \o (T \o S)] ~> [the functor of T \o S].
  apply: (VComp ((@join T) \h (@join S)) _).
  apply VA.
  apply AV.
  apply HComp.
(*  exact: NId.*)admit.
  apply VA'.
  apply AV'.
  apply HComp.
  exact: f.
(*  exact: NId.*) admit.
apply: (Monad.Pack (Monad.Class (isMonad.Axioms_ (CRet T S) join _ _ _ _ _))).
move=> A.
rewrite /join.
Abort.

author: affeldt-aist

repo: monae

save_path: github-repos/coq/affeldt-aist-monae


text:
Require Import Omega String Ascii.
Require Import Coq.Structures.OrderedType.

Lemma nat_compare_eq_refl : forall x, nat_compare x x = Eq.
  intros; apply nat_compare_eq_iff; trivial.
Qed.

Hint Rewrite <- nat_compare_lt : nat_comp_hints.
Hint Rewrite <- nat_compare_gt : nat_comp_hints.
Hint Rewrite    nat_compare_eq_iff : nat_comp_hints.
Hint Rewrite <- nat_compare_eq_iff : nat_comp_hints.
Hint Rewrite    nat_compare_eq_refl : nat_comp_hints.

Ltac autorewrite_nat_compare :=
  autorewrite with nat_comp_hints in *.

Lemma nat_compare_consistent :
  forall n0 n1,
    { nat_compare n0 n1 = Lt /\ nat_compare n1 n0 = Gt }
    + { nat_compare n0 n1 = Eq /\ nat_compare n1 n0 = Eq }
    + { nat_compare n0 n1 = Gt /\ nat_compare n1 n0 = Lt }.
Proof.
  intros n0 n1;
  destruct (lt_eq_lt_dec n0 n1) as [ [_lt | _eq] | _lt ];
  [ constructor 1; constructor 1  | constructor 1; constructor 2 | constructor 2 ];
  split;
  autorewrite_nat_compare;
  intuition.
Qed.

Module String_as_OT <: OrderedType.
  Definition t := string.

  Fixpoint string_compare str1 str2 :=
    match str1, str2 with
      | EmptyString, EmptyString => Eq
      | EmptyString, _           => Lt
      | _, EmptyString           => Gt
      | String char1 tail1, String char2 tail2 =>
        match nat_compare (nat_of_ascii char1) (nat_of_ascii char2) with
          | Eq => string_compare tail1 tail2
          | Lt => Lt
          | Gt => Gt
        end
    end.

  Lemma string_compare_eq_refl : forall x, string_compare x x = Eq.
    intro x;
    induction x;
      simpl; trivial;
      autorewrite_nat_compare.
      trivial.
  Qed.

  Ltac comparisons_minicrush :=
    autorewrite_nat_compare;
    match goal with
      | [ |- context [nat_compare ?a ?b] ] =>
        let H := fresh in
        first [
            assert (nat_compare a b = Eq) as H by (autorewrite_nat_compare; omega) |
            assert (nat_compare a b = Lt) as H by (autorewrite_nat_compare; omega) |
            assert (nat_compare a b = Gt) as H by (autorewrite_nat_compare; omega)
        ]; rewrite H; intuition
    end.

  Ltac destruct_comparisons :=
    repeat match goal with
             | [ H: match ?pred ?a ?b with
                      | Lt => _ | Gt => _ | Eq => _ end = _
                 |- _] =>
               let H := fresh in
               destruct (pred a b) eqn:H;
                 try discriminate
           end.

  Ltac exfalso_from_equalities :=
    match goal with
      | [ H1: ?a = ?b, H2: ?a = ?c |- _ ] => assert (b = c) by congruence; discriminate
    end.

  Definition eq := @eq string.

  Hint Resolve string_compare_eq_refl.

  Lemma eq_Eq : forall x y, x = y -> string_compare x y = Eq.
  Proof.
    intros; subst; auto.
  Qed.

  Lemma nat_of_ascii_injective :
    forall a b, nat_of_ascii a = nat_of_ascii b <-> a = b.
  Proof.
    intros a b; split; intro H;
    [ apply (f_equal ascii_of_nat) in H;
      repeat rewrite ascii_nat_embedding in H
    | apply (f_equal nat_of_ascii) in H ]; trivial.
  Qed.

  Lemma Eq_eq : forall x y, string_compare x y = Eq -> x = y.
  Proof.
    induction x;
      destruct y;
      simpl;
      first [ discriminate
            | intros;
              f_equal;
              destruct_comparisons;
              autorewrite_nat_compare;
              rewrite nat_of_ascii_injective in *
            | idtac ];
      intuition.
  Qed.

  Lemma Eq_eq_iff : forall x y, x = y <-> string_compare x y = Eq.
  Proof.
    intros; split; eauto using eq_Eq, Eq_eq.
  Qed.

  Definition eq_refl := @eq_refl string.

  Definition eq_sym := @eq_sym string.

  Definition eq_trans := @eq_trans string.

  Definition lt x y :=
    string_compare x y = Lt.

  Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
  Proof.
    intros x y z;
    generalize x z;
    clear x z;

    induction y;
    destruct x;
    destruct z;
      intros;
      unfold lt in *;
      simpl in *;
      first [ discriminate
            | destruct_comparisons; comparisons_minicrush
            | trivial ]; intuition.
  Qed.

  Lemma lt_not_eq : forall x y, lt x y -> ~ eq x y.
  Proof.
    unfold lt, not in *;
    intros;
    rewrite Eq_eq_iff in *;
    exfalso_from_equalities.
  Qed.

  Lemma Lt_Gt : forall x y, string_compare x y = Gt <-> string_compare y x = Lt.
  Proof.
    intros x;
    induction x as [ | x0 x' Hind ];
      intros y;
      destruct y as [ | y0 y' ];

      simpl;
      split;
      first [ discriminate | trivial ];

      destruct (nat_compare_consistent
                  (nat_of_ascii x0)
                  (nat_of_ascii y0))
          as [ [ (H1, H2) | (H1, H2) ] | (H1, H2) ];
        rewrite H1, H2;
        try rewrite Hind;
        auto.
  Qed.

  Definition compare x y : OrderedType.Compare lt eq x y.
  Proof.
    destruct (string_compare x y) eqn:comp;
      unfold lt;
      [ constructor 2; apply Eq_eq
      | constructor 1
      | constructor 3; apply Lt_Gt];
      trivial.
  Defined.

  Definition eq_dec : forall (x y: string), { x = y } + { x <> y }.
  Proof.
    intros;
    destruct (string_compare x y) eqn:eq0;
      first [
          left;
          apply Eq_eq;
          solve [trivial]
        | right;
          unfold not;
          rewrite Eq_eq_iff;
          intros;
          exfalso_from_equalities
        ].
  Qed.
End String_as_OT.

(* Usage example:
Require Import FMapAVL.
Require Import Coq.Structures.OrderedTypeEx.

Module StringIndexedMap := FMapAVL.Make(String_as_OT).
Definition String2Nat := StringIndexedMap.t nat.

Definition find key (map: String2Nat) := StringIndexedMap.find key map.

Definition bind (pair: string * nat) (map: String2Nat) := StringIndexedMap.add (fst pair) (snd pair) map.

Notation "k >> v" := (pair k v) (at level 100).
Notation "[[ b1 , .. , bn ]]" := (bind b1 .. (bind bn (StringIndexedMap.empty nat)) .. ).

Open Scope string.

Definition population_in_millions :=
 [[ "china" >> 1364, "india" >> 1243, "united states" >> 318, "indonesia" >> 247, "brazil" >> 201, "pakistan" >> 186, "nigeria" >> 174, "bangladesh" >> 153, "russia" >> 144, "japan" >> 127, "mexico" >> 120, "philippines" >> 99, "vietnam" >> 90, "ethiopia" >> 87, "egypt" >> 86, "germany" >> 81, "iran" >> 77, "turkey" >> 77, "democratic republic of the congo" >> 68, "france" >> 66 ]].

Eval compute in (find "france" population_in_millions).
*)

author: JasonGross

repo: adt-synthesis