text:
(************************************************************************)
(* Copyright (c) 2010, Martijn Vermaat <martijn@vermaat.name>           *)
(*                                                                      *)
(* Licensed under the MIT license, see the LICENSE file or              *)
(* http://en.wikipedia.org/wiki/Mit_license                             *)
(************************************************************************)

(** This library defines the type [ord] of tree ordinals.

   This formalisation of tree ordinals is based on notes by Peter Hancock:

     (Ordinal-theoretic) Proof Theory.
     Course notes from Midlands Graduate School, 2008.

     % \url{http://personal.cis.strath.ac.uk/~ph/} %
     # http://personal.cis.strath.ac.uk/~ph/ #

     % http://events.cs.bham.ac.uk/mgs2008/notes/proofTheory.pdf %
     # http://events.cs.bham.ac.uk/mgs2008/notes/proofTheory.pdf #

  See also the formalisation in Isabelle by Michael Compton:
  % http://www4.informatik.tu-muenchen.de/~isabelle/html-data/library/HOL/Induct/Tree.html %
  # http://www4.informatik.tu-muenchen.de/~isabelle/html-data/library/HOL/Induct/Tree.html #
*)

Set Implicit Arguments.

Delimit Scope ord_scope with ord.
Open Scope ord_scope.

(** Inductive type for tree ordinals. *)
Inductive ord : Set :=
  | Zero  : ord
  | Succ  : ord -> ord
  | Limit : (nat -> ord) -> ord.

(** The intuition is that the [Limit] constructor represents the least
   upper bound of its argument sequence.

   We might like to exclude sequences such as (4,4,4,...), since they would
   not necessarily represent a limit ordinal. A way to do this is by
   imposing a monotonicity property on the [Limit] arguments. We first
   define an ordering on [ord] and, using that, define a subset of [ord]
   where the [Limit] arguments are monotone (in library [WfOrdinal]). *)

(** Type of predecessor indices of an ordinal. *)
Fixpoint pd_type (alpha : ord) : Set :=
  match alpha with
  | Zero       => False
  | Succ alpha => (unit + pd_type alpha) % type
  | Limit f    => { n : nat & pd_type (f n) }
  end.

Reserved Notation "alpha [ i ]" (at level 60).

(** Predecessor indices of an ordinal are essentially the paths on its tree
   structure starting from the root that cross at least one [Succ]
   constructor. *)

(** Predecessor of an ordinal for a given predecessor index. *)
Fixpoint pd (alpha : ord) : pd_type alpha -> ord :=
  match alpha with
  | Zero       => False_rect _
  | Succ alpha => fun i => match i with
                           | inl tt => alpha
                           | inr t  => alpha[t]
                           end
  | Limit f    => fun i => match i with
                           | existT n t => (f n)[t]
                           end
  end
where "alpha [ i ]" := (pd alpha i) : ord_scope.

(** [pd_type] and [pd] can be seen as defining a 'subtree' partial order on
   [ord]. We use it to define an extensional non-strict order on [ord]. *)

(** Non-strict order on [ord]. *)
Inductive ord_le : ord -> ord -> Prop :=
  | Ord_le_Zero  : forall beta,
                      Zero <= beta
  | Ord_le_Succ  : forall alpha beta i,
                      alpha <= beta[i] ->
                      Succ alpha <= beta
  | Ord_le_Limit : forall f beta,
                      (forall n, f n <= beta) ->
                      Limit f <= beta
where "alpha <= beta" := (ord_le alpha beta) : ord_scope.

(** Strict order on [ord]. *)
Definition ord_lt (alpha beta : ord) := exists i, alpha <= beta[i].
Infix " < " := ord_lt : ord_scope.

(** Equality on [ord]. *)
Definition ord_eq alpha beta := alpha <= beta /\ beta <= alpha.
Infix " == " := ord_eq (no associativity, at level 75) : ord_scope.

(** We proceed with some useful lemmas about these relations. *)

(** First predecessor of a successor is the original ordinal. *)
Lemma first_pd_after_succ_id :
  forall alpha, alpha = Succ alpha [inl (pd_type alpha) tt].
Proof.
trivial.
Qed.

(** No successor ordinal <= zero. *)
Lemma ord_le_not_succ_zero :
  forall alpha, ~ Succ alpha <= Zero.
Proof.
intros alpha H.
inversion_clear H.
destruct i.
Qed.

(** No double successor <= 1. *)
Lemma ord_le_not_succ_succ_one :
  forall alpha, ~ Succ (Succ alpha) <= Succ Zero.
Proof.
intros alpha H.
inversion_clear H.
destruct i.
destruct u.
apply (@ord_le_not_succ_zero alpha).
assumption.
assumption.
Qed.

(** If alpha <= zero, alpha <= any ordinal. *)
Lemma ord_le_zero_right :
  forall alpha beta,
    alpha <= Zero ->
    alpha <= beta.
Proof.
induction alpha as [| alpha _ | f IH]; intros beta H.
constructor.
inversion_clear H.
destruct i.
inversion_clear H.
constructor.
intro n.
apply IH.
trivial.
Qed.

(** If alpha <= a predecessor of beta, alpha <= beta. *)
Lemma ord_le_pd_right :
  forall alpha beta (i : pd_type beta),
    alpha <= beta[i] ->
    alpha <= beta.
Proof.
induction alpha as [| alpha IH | f IH]; intros beta i H.
constructor.
apply Ord_le_Succ with i.
inversion H as [| a b j |].
apply IH with j.
assumption.
constructor.
intro n.
inversion_clear H.
apply IH with i.
trivial.
Qed.

(** If alpha <= beta, all predecessors of alpha <= beta. *)
Lemma ord_le_pd_left :
  forall alpha beta (i : pd_type alpha),
    alpha <= beta ->
    alpha[i] <= beta.
Proof.
intros alpha beta i H.
induction H as [| alpha beta j H IH | f beta H IH].
destruct i.
destruct i as [[] | i']; apply ord_le_pd_right with j.
apply H.
apply IH.
destruct i.
apply IH.
Qed.

(** If alpha <= beta, alpha <= the successor of beta. *)
Lemma ord_le_succ_right :
  forall alpha beta,
    alpha <= beta ->
    alpha <= Succ beta.
Proof.
induction alpha as [| alpha _ | f IH]; intros beta H.
constructor.
inversion_clear H.
apply Ord_le_Succ with (inr unit i).
assumption.
constructor.
intro n.
apply IH.
inversion_clear H.
trivial.
Qed.

(** If the successor of alpha <= beta, alpha <= beta. *)
Lemma ord_le_succ_left :
  forall alpha beta,
    Succ alpha <= beta ->
    alpha <= beta.
Proof.
intros alpha beta H.
rewrite (first_pd_after_succ_id alpha).
apply ord_le_pd_left.
assumption.
Qed.

(** If the successor of alpha <= the successor of beta, alpha <= beta. *)
Lemma ord_le_succ_elim :
  forall alpha beta,
    Succ alpha <= Succ beta ->
    alpha <= beta.
Proof.
inversion_clear 1.
destruct i as [[] |]; [| apply ord_le_pd_right with p]; assumption.
Qed.

(** If the alpha <= beta, the successor of alpha <= the successor of beta. *)
Lemma ord_le_succ_intro :
  forall alpha beta,
    alpha <= beta ->
    Succ alpha <= Succ beta.
Proof.
intros.
apply Ord_le_Succ with (inl (pd_type beta) tt).
assumption.
Qed.

(** No successor of alpha is <= alpha. *)
Lemma ord_le_not_succ :
  forall alpha, ~ Succ alpha <= alpha.
Proof.
induction alpha as [| alpha IH | f IH]; intro H.
apply ord_le_not_succ_zero with Zero.
assumption.
apply IH.
exact (ord_le_succ_elim H).
inversion_clear H as [| a b i H' |].
inversion_clear H' as [| | a b H].
destruct i as [n i].
apply IH with n.
apply Ord_le_Succ with i.
apply H.
Qed.

(** If alpha <= a function value, alpha <= the limit of that function.
   Suggested by Bruno Barras. *)
Lemma ord_le_limit_right :
  forall alpha f n,
    alpha <= f n ->
    alpha <= Limit f.
Proof.
induction alpha as [| alpha _ | f IH]; intros g n H.
constructor.
inversion_clear H.
apply Ord_le_Succ with (existT (fun n => pd_type (g n)) n i).
assumption.
constructor.
intro m.
apply (IH m g n).
inversion_clear H.
trivial.
Qed.

(** If a limit <= alpha, any value value of the function <= alpha. *)
Lemma ord_le_limit_left :
  forall alpha f n,
    Limit f <= alpha ->
    f n <= alpha.
Proof.
intros alpha f n H.
inversion_clear H.
trivial.
Qed.

(** [<=] is reflexive. *)
Lemma ord_le_refl :
  forall alpha, alpha <= alpha.
Proof.
induction alpha as [| alpha IH | f IH].
constructor.
apply Ord_le_Succ with (inl (pd_type alpha) tt).
assumption.
constructor.
intro n.
apply ord_le_limit_right with n.
apply IH.
Qed.

(** [<=] is transitive. *)
Lemma ord_le_trans :
  forall alpha beta gamma,
    alpha <= beta ->
    beta <= gamma ->
    alpha <= gamma.
Proof.
intros alpha beta gamma H1.
revert gamma.
induction H1 as [| alpha beta i H IH | f beta H IH]; intros gamma H2.
constructor.
induction H2 as [| beta gamma j H' _ | f gamma H' IH'].
destruct i.
apply Ord_le_Succ with j.
apply IH.
destruct i as [[] | i']; simpl in * |- *.
assumption.
apply ord_le_pd_left.
assumption.
destruct i as [n i]; simpl in * |- *.
apply (IH' n i H IH).
constructor.
intro n.
exact (IH n gamma H2).
Qed.

(** [<=] is antisymmetric (for [==]). *)
Lemma ord_le_antisymm :
  forall alpha beta,
    alpha <= beta ->
    beta <= alpha ->
    alpha == beta.
Proof.
intros.
unfold ord_eq.
split; assumption.
Qed.

(* TODO: Can we prove <= is total? *)

(** [==] is reflexive. *)
Lemma ord_eq_refl :
  forall alpha, alpha == alpha.
Proof.
split; apply ord_le_refl.
Qed.

(** [==] is symmetric. *)
Lemma ord_eq_symm :
  forall alpha beta,
    alpha == beta ->
    beta == alpha.
Proof.
split; apply H.
Qed.

(** [==] is transitive. *)
Lemma ord_eq_trans :
  forall alpha beta gamma,
    alpha == beta ->
    beta == gamma ->
    alpha == gamma.
Proof.
destruct 1.
destruct 1.
split; apply ord_le_trans with beta; assumption.
Qed.

(** Not zero < zero. *)
Lemma ord_lt_zero_zero :
  ~ Zero < Zero.
Proof.
intro H.
destruct H as [i H].
elim i.
Qed.

(** If alpha <= beta, not beta <= a predecessor of alpha. *)
Lemma ord_le_not_pd_right :
  forall alpha beta i,
    alpha <= beta ->
    ~ beta <= alpha[i].
Proof.
induction alpha as [| alpha IH | f IH]; intros beta i H1 H2.
destruct i.
destruct i.
destruct u.
apply ord_le_not_succ with alpha.
apply ord_le_trans with beta; assumption.
exact (IH beta p (ord_le_succ_left H1) H2).
destruct i.
inversion_clear H1.
exact (IH x beta p (H x) H2).
Qed.

(** Not alpha <= a predecessor of alpha. *)
Lemma ord_le_not_pd_right_weak :
  forall alpha i, ~ alpha <= alpha[i].
Proof.
intros.
apply ord_le_not_pd_right.
apply ord_le_refl.
Qed.

(** [<] is transitive. *)
Lemma ord_lt_trans :
  forall alpha beta gamma,
    alpha < beta ->
    beta < gamma ->
    alpha < gamma.
Proof.
intros alpha beta gamma.
destruct 1 as [i].
destruct 1 as [j].
exists j.
apply ord_le_trans with beta; [apply ord_le_pd_right with i |]; assumption.
Qed.

(** [<] is irreflexive. *)
Lemma ord_lt_irrefl :
  forall alpha, ~ alpha < alpha.
Proof.
intros alpha H.
destruct H as [i H].
exact (ord_le_not_pd_right_weak i H).
Qed.

(** [<] is asymmetric. *)
Lemma ord_lt_asymm :
  forall alpha beta,
    alpha < beta ->
    ~ beta < alpha.
Proof.
intros alpha beta H1 H2.
destruct H1 as [i H1].
destruct H2 as [j H2].
apply (@ord_le_not_pd_right alpha beta j);
  [apply ord_le_pd_right with i |]; assumption.
Qed.

(** [pd_type] is closed under transitivity. *)
Lemma pd_trans :
  forall alpha i j,
    exists k, pd alpha k = pd (pd alpha i) j.
Proof.
induction alpha as [| alpha IH | f IH]; intros.
elim i.
destruct i as [[] | i]; simpl in j |- *.
exists (inr _ j).
reflexivity.
destruct (IH i j) as [k H].
exists (inr _ k).
assumption.
destruct i as [n i]; simpl in j |- *.
destruct (IH n i j) as [k H].
exists (existT (fun n => pd_type (f n)) n k).
assumption.
Qed.

(** If the successor of alpha < beta, alpha < beta. *)
Lemma ord_lt_succ_left :
  forall alpha beta,
    Succ alpha < beta ->
    alpha < beta.
Proof.
intros alpha beta.
destruct 1 as [i H].
exists i.
apply ord_le_succ_left.
assumption.
Qed.

(** If alpha < beta, alpha < the successor of beta. *)
Lemma ord_lt_succ_right :
  forall alpha beta,
    alpha < beta ->
    alpha < Succ beta.
Proof.
intros alpha beta.
destruct 1 as [i H].
exists (inl (pd_type beta) tt).
apply ord_le_pd_right with i.
assumption.
Qed.

(** If alpha < beta, alpha <= beta. *)
Lemma ord_lt_ord_le :
  forall alpha beta, alpha < beta -> alpha <= beta.
Proof.
intros alpha beta.
destruct 1 as [i H].
apply ord_le_pd_right with i.
assumption.
Qed.

(** If alpha < beta, the successor of alpha <= beta. *)
Lemma ord_lt_ord_le_succ :
  forall alpha beta,
    alpha < beta ->
    Succ alpha <= beta.
Proof.
intros alpha beta.
destruct 1 as [i H].
apply Ord_le_Succ with i.
assumption.
Qed.

(** If alpha < beta, not beta <= alpha. *)
Lemma ord_lt_not_ord_le :
  forall alpha beta,
    alpha < beta ->
    ~ beta <= alpha.
Proof.
intros alpha beta H1 H2.
destruct H1 as [i H1].
apply (@ord_le_not_pd_right beta alpha i); assumption.
Qed.

(** If alpha <= a predecessor of the successor of beta, alpha <= beta. *)
Lemma ord_le_succ_pd_right :
  forall alpha beta i,
    alpha <= Succ beta [i] ->
    alpha <= beta.
Proof.
(* This is a messy proof *)
induction alpha; intros.
simpl in H.
destruct i.
destruct u.
assumption.
apply Ord_le_Zero.
destruct beta.
destruct i.
destruct u.
destruct (ord_le_not_succ_zero H).
destruct p.
apply Ord_le_Succ with (inl (pd_type beta) tt).
simpl.
simpl in H.
destruct i.
destruct u.
apply ord_le_succ_elim.
assumption.
destruct p.
apply ord_le_succ_left.
destruct u.
assumption.
apply ord_le_succ_left.
apply ord_le_pd_right with p.
assumption.
simpl in H.
destruct i.
destruct u.
assumption.
destruct p.
apply ord_le_limit_right with x.
apply ord_le_pd_right with p.
assumption.
apply Ord_le_Limit.
intro.
inversion_clear H0.
apply H with i.
apply H1.
Qed.

(** Ordinal arithmetic. *)

Fixpoint add (alpha beta : ord) : ord :=
  match beta with
  | Zero      => alpha
  | Succ beta => Succ (add alpha beta)
  | Limit f   => Limit (fun o => add alpha (f o))
  end.

Fixpoint mul (alpha beta : ord) : ord :=
  match beta with
  | Zero      => Zero
  | Succ beta => add (mul alpha beta) alpha
  | Limit f   => Limit (fun o => mul alpha (f o))
  end.

Fixpoint exp (alpha beta : ord) : ord :=
  match beta with
  | Zero      => Succ Zero
  | Succ beta => mul (exp alpha beta) alpha
  | Limit f   => Limit (fun o => exp alpha (f o))
  end.

Lemma ord_le_add_right :
  forall alpha beta,
    alpha <= add alpha beta.
Proof.
intros alpha beta.
induction beta as [| beta IH | f IH].
apply ord_le_refl.
apply ord_le_succ_right.
exact IH.
apply ord_le_limit_right with 0.
apply IH.
Qed.

Lemma ord_le_add :
  forall alpha beta gamma,
    beta <= gamma ->
    add alpha beta <= add alpha gamma.
Proof.
intros alpha beta gamma H.
induction H as [gamma | beta gamma i H IH | f gamma H IH].
apply ord_le_add_right.
induction gamma as [| gamma IHg | f IHg]; simpl.
elim i.
destruct i as [[] | i].
apply Ord_le_Succ with (inl (pd_type (add alpha gamma)) tt).
apply IH.
apply ord_le_succ_right.
apply IHg with i; assumption.
destruct i as [n i].
apply ord_le_limit_right with n.
apply IHg with i; assumption.
constructor.
intro n.
apply IH.
Qed.

Lemma ord_lt_add :
  forall alpha beta gamma,
    beta < gamma ->
    add alpha beta < add alpha gamma.
Proof.
intros alpha beta gamma H.
unfold ord_lt; destruct H as [i H].
induction gamma as [| gamma _ | f IH]; simpl.
destruct i.
exists (inl _ tt); simpl.
apply ord_le_add.
destruct i as [[] | i].
assumption.
apply ord_le_pd_right with i.
assumption.
destruct i as [n i].
specialize IH with n i.
destruct IH as [j IH].
assumption.
exists (existT (fun n => pd_type (add alpha (f n))) n j).
assumption.
Qed.

(** The natural numbers can be coerced into finite ordinals. *)

Fixpoint nat_as_ord (n : nat) : ord :=
  match n with
  | O   => Zero
  | S n => Succ (nat_as_ord n)
  end.

Coercion nat_as_ord : nat >-> ord.

(** The smallest infinite ordinal is the limit of the natural numbers. *)
Definition omega := Limit (fun n => n).

(** We show that [<=] and [<] on ordinals are the same as [<=] and [<] on
   natural numbers. *)

Require Import Le.

Lemma le_implies_ord_le : forall n m, (n <= m)%nat -> n <= m.
Proof.
induction n as [| n IH]; intros m H.
constructor.
destruct m as [| m].
contradiction le_Sn_0 with n.
apply ord_le_succ_intro.
apply IH.
apply le_S_n.
assumption.
Qed.

Lemma ord_le_implies_le : forall (n m : nat), n <= m -> (n <= m)%nat.
Proof.
induction n as [| n IH]; intros m H.
apply le_0_n.
destruct m as [| m].
contradiction ord_le_not_succ_zero with n.
apply le_n_S.
apply IH.
apply ord_le_succ_elim.
assumption.
Qed.

Lemma ord_le_le : forall n m, (n <= m)%nat <-> n <= m.
Proof.
split.
apply le_implies_ord_le.
apply ord_le_implies_le.
Qed.

Require Import Lt.

Lemma lt_implies_ord_lt : forall n m, (n < m)%nat -> n < m.
Proof.
induction n as [| n IH]; intros m H.
destruct H; exists (inl _ tt); constructor.
destruct m as [| m].
contradiction lt_n_O with (S n).
exists (inl _ tt).
apply ord_lt_ord_le_succ; simpl.
apply IH.
apply lt_S_n.
assumption.
Qed.

Lemma ord_lt_implies_lt : forall (n m : nat), n < m -> (n < m)%nat.
Proof.
induction n as [| n IH]; intros m H.
destruct H as [i H].
destruct m as [| m].
elim i.
apply lt_0_Sn.
destruct H as [i H].
destruct m as [| m].
elim i.
apply lt_n_S.
apply IH.
(* this can be cleaned up *)
destruct m as [| m].
destruct i as [[] | []].
contradiction ord_le_not_succ_zero with n.
exists (inl _ tt).
destruct i as [[] | [[] | i]].
apply ord_le_succ_elim.
assumption.
apply ord_le_succ_left.
assumption.
apply ord_le_succ_left.
apply ord_le_pd_right with i.
assumption.
Qed.

Lemma ord_lt_lt : forall n m, (n < m)%nat <-> n < m.
Proof.
split.
apply lt_implies_ord_lt.
apply ord_lt_implies_lt.
Qed.

(** We now prove two simple facts about our equality [==] containing
   different representations of omega. *)

Lemma fact_a :
  Limit (fun n => S n) == omega.
Proof.
split; constructor; intro n.
apply Ord_le_Succ with (existT (fun n:nat => pd_type n) (S n) (inl _ tt)).
apply ord_le_refl.
destruct n as [| n].
constructor.
apply Ord_le_Succ with (existT (fun n:nat => pd_type (S n)) n (inl _ tt)).
apply ord_le_refl.
Qed.

Lemma fact_b :
  Limit (fun n => n * 2) == omega.
Proof.
split; constructor; intro n.
destruct n as [| n]; simpl.
constructor.
apply Ord_le_Succ with (existT (fun n:nat => pd_type n) (S (S (n * 2))) (inl _ tt)).
apply ord_le_refl.
destruct n as [| n].
constructor.
apply Ord_le_Succ with (existT (fun n:nat => pd_type (n * 2)) (S n) (inl _ tt)).
simpl.
induction n as [| n IH]; simpl.
constructor.
apply ord_le_succ_right.
apply ord_le_succ_intro.
exact IH.
Qed.

(** A weak inversion property of ordinals equal to omega. *)
Lemma ord_eq_omega_discriminate :
  forall alpha,
    alpha == omega ->
    exists f, alpha = Limit f.
Proof.
intros [| alpha | f] [H1 H2].
inversion_clear H2.
contradict (ord_le_not_succ_zero (H 1)).
inversion_clear H1.
inversion_clear H2.
destruct i as [n i].
contradict (ord_le_not_pd_right i (ord_le_succ_elim (H0 (S n))) H).
exists f; reflexivity.
Qed.

Close Scope ord_scope.

author: martijnvermaat

repo: infinitary-rewriting-coq


text:
(* example thanks to Jonathan Leivent, Dec 2, 2016 email to coq-club

(subject Re: [Coq-Club] Unification Bug?)

https://sympa.inria.fr/sympa/arc/coq-club/2016-12/msg00007.html

 *)
Definition foo A B : (A -> B) = (A -> B) := eq_refl.

Goal { T:Type | T=T }.
   refine (exist _ (forall (x:?[T1]), ?[T2]) _).
   instantiate (T2:=ltac:(clear x)). (*remove dependency of ?T2 on x*)
   apply foo.

   Unshelve.
   all: exact nat.
Qed.

author: tchajed

repo: coq-tricks

save_path: github-repos/coq/tchajed-coq-tricks


text:
(** Coq configuration for std++ (not meant to leak to clients) *)
(* Everything here should be [Export Set], which means when this
file is *imported*, the option will only apply on the import site
but not transitively. *)

Export Set Default Proof Using "Type".
(* FIXME: cannot enable this yet as some files disable 'Default Proof Using'.
Export Set Suggest Proof Using. *)
(* FIXME: cannot enable this on Coq 8.8.
Export Set Default Goal Selector "!". *)

(* "Fake" import to whitelist this file for the check that ensures we import
this file everywhere.
From stdpp Require Import options.
*)

author: SkySkimmer

repo: stdpp

save_path: github-repos/coq/SkySkimmer-stdpp


text:
Require Import Category.Lib.
Require Import Category.Theory.

Require Import Core.Basics.
Require Import Core.Tagged.
Require Import Core.HVec.
Require Export FOL.Signature.
Require Export FOL.Algebra.
Require Export FOL.Sentence.
Require Export Lib.Institutions.

Require Import Coq.Program.Equality.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import ProofIrrelevance.
Require Import FunInd.

Import EqNotations.

(*****************************************************************************)
(** * First-Order Signature Category *)

Definition id_arityF_tm [T : Type] (X : Tagged (list T * T)) :
  tagged_morphism (lift_sig idmap) X X.
Proof.
  refine (exist _ idmap _); intros.
  unfold lift_sig. rewrite map_id.
  now induction (X x).
Defined.

Definition id_arityP_tm [T : Type] (X : Tagged (list T)) :
  tagged_morphism (map idmap) X X.
Proof.
  refine (exist _ idmap _); intros.
  now rewrite map_id.
Defined.

Definition id_FOSig (Σ : Signature) : SignatureMorphism Σ Σ := {|
  on_sorts := idmap ;
  on_funcs := id_arityF_tm (Funcs Σ) ;
  on_preds := id_arityP_tm (Preds Σ) ;
|}.

Program Definition comp_FOSig
    {A B C : Signature}
    (τ : SignatureMorphism B C)
    (σ : SignatureMorphism A B)
    : SignatureMorphism A C := {|
  on_sorts := τ ∘ σ ;
  on_funcs := tagged_morphism_compose (on_funcs τ) (on_funcs σ) ;
  on_preds := tagged_morphism_compose (on_preds τ) (on_preds σ) ;
|}.
Next Obligation. repeat rewrite tagged_morphism_commutes. now rewrite lift_sig_compose. Defined.
Next Obligation. repeat rewrite tagged_morphism_commutes. now rewrite map_map. Defined.

Theorem id_left_FOSig {Σ Σ'} (σ : SignatureMorphism Σ Σ') :
  comp_FOSig (id_FOSig Σ') σ = σ.
Proof with cbn.
  apply (eq_signature_morphism _ _ (comp_FOSig (id_FOSig Σ') σ) σ eq_refl);
  cbn; apply tagged_morphism_eq; easy.
Qed.

Theorem id_right_FOSig {Σ Σ'} (σ : SignatureMorphism Σ Σ') :
  comp_FOSig σ (id_FOSig Σ) = σ.
Proof with cbn.
  apply (eq_signature_morphism _ _ (comp_FOSig σ (id_FOSig Σ)) σ eq_refl); cbn;
  apply tagged_morphism_eq; easy.
Qed.

Lemma comp_assoc_FOSig
    (A B C D : Signature)
    (h : SignatureMorphism C D)
    (g : SignatureMorphism B C)
    (f : SignatureMorphism A B) :
  comp_FOSig h (comp_FOSig g f) = comp_FOSig (comp_FOSig h g) f.
Proof with cbn.
  apply (eq_signature_morphism _ _
    (comp_FOSig h (comp_FOSig g f))
    (comp_FOSig (comp_FOSig h g) f) eq_refl
  ); cbn; apply tagged_morphism_eq; easy.
Qed.

Lemma comp_assoc_sym_FOSig :
  ∀ (A B C D : Signature)
    (h : SignatureMorphism C D)
    (g : SignatureMorphism B C)
    (f : SignatureMorphism A B),
  comp_FOSig (comp_FOSig h g) f = comp_FOSig h (comp_FOSig g f).
Proof.
  symmetry; apply comp_assoc_FOSig.
Qed.

Definition FOSig : Category := {|
  obj := Signature ;
  hom := SignatureMorphism ;
  homset := Morphism_equality ;
  id := id_FOSig ;
  compose  := @comp_FOSig ;
  id_left  := @id_left_FOSig ;
  id_right := @id_right_FOSig ;
  comp_assoc := comp_assoc_FOSig ;
  comp_assoc_sym := comp_assoc_sym_FOSig ;
|}.

(*****************************************************************************)
(** * First-Order Sentence Functor *)

Lemma reindex_member_id :
  ∀ (Σ : Signature) (Γ : Ctx Σ) (s : Sorts Σ) (m : member s Γ),
  reindex_member idmap m = rew (map_id Γ)^ in m.
Proof.
  intros; induction m; cbn.
  - rewrite map_id_cons_pfs.
    rewrite <- ap_V.
    now destruct (map_id is)^.
  - rewrite map_id_cons_pfs.
    rewrite <- ap_V.
    rewrite <- rew_map.
    rewrite IHm.
    now rewrite lemma2_3_11.
Qed.

Lemma reindex_member_comp :
  ∀ {I J K : Type} (f : I -> J) (g : J -> K)
    {i : I} {is : list I} (m : member i is),
  reindex_member (g ∘ f) m =
    rew (map_map f g is) in reindex_member g (reindex_member f m).
Proof.
  intros.
  induction m; cbn.
  - rewrite map_map_cons_pfs.
    rewrite <- rew_map.
    now destruct (map_map f g is).
  - rewrite map_map_cons_pfs.
    rewrite <- rew_map.
    now rewrite lemma2_3_11, <- IHm.
Qed.

Lemma reindex_id :
  ∀ {I : Type} {A : I -> Type}
    {is : list I} (args : HVec A is),
  reindex idmap args = rew (map_id is)^ in args.
Proof.
  induction args; cbn in *.
  - now simplify_eqs.
  - rewrite IHargs.
    rewrite map_id_cons_pfs.
    rewrite <- ap_V.
    now case (map_id is)^.
Qed.

Lemma reindex_comp :
  ∀ {I J K : Type} {A : K -> Type} {is : list I}
    (f : I -> J) (g : J -> K) (args : HVec (A ∘ (g ∘ f)) is),
  rew map_map f g is in reindex g (reindex f args) = reindex (g ∘ f) args.
Proof.
  induction args; cbn in *.
  - now simplify_eqs.
  - rewrite <- IHargs. simplify_eqs. destruct eqH0. now simplify_eqs.
Qed.

Definition on_terms_id Σ Γ s (t : Term Σ Γ s) :
  on_terms (id_FOSig Σ) t = rew [λ Γ, Term Σ Γ s] (map_id Γ)^ in t.
Proof.
  induction t using term_ind'.
  - simp on_terms; rewrite (map_subst (λ _, var)).
    now rewrite reindex_member_id.
  - simp on_terms.
    simpl on_funcs.
    rewrite map_on_terms_hmap; cbn.
    rewrite reindex_id; cbn. rewrite rew_compose.
    revert H; simplify_eqs; intros H.
    pose proof (H' := proj1 (map_ext_HForall _ _ _) H).
    setoid_rewrite H'.
    case eqH. cbn. now rewrite hmap_id.
Qed.

Theorem map_on_terms_id Σ Γ w (ts : HVec (Term Σ Γ) w) :
  map_on_terms (id_FOSig Σ) ts =
    rew [λ w, HVec (Term Σ (map idmap Γ)) w] (map_id w)^ in
      (rew [λ Γ, HVec (Term Σ Γ) w] (map_id Γ)^ in ts).
Proof with cbn.
  rewrite map_on_terms_hmap; cbn in *.
  induction ts.
  - now simplify_eqs.
  - rewrite map_id_cons_pfs.
    rewrite rew_map...
    rewrite on_terms_id.
    rewrite <- ap_V, f_equal_compose.
    rewrite <- rew_map.
    rewrite IHts.
    now simplify_eqs.
Qed.

Fixpoint on_terms_comp
    {A B C : Signature}
    (σ : SignatureMorphism A B) (τ : SignatureMorphism B C)
    {Γ : Ctx A} {s : Sorts A} (t : Term A Γ s) :
  rew [λ Γ, Term C Γ _] (map_map σ τ Γ) in
    (on_terms τ (on_terms σ t)) = on_terms (comp_FOSig τ σ) t.
Proof.
  - induction t using term_ind'.
    * simp on_terms; cbn.
      rewrite (reindex_member_comp σ τ m).
      rewrite (map_subst (P := member (τ (σ s))) (λ _, var)); auto.
    * simp on_terms.
      cut (∀ (A B C : Signature)
             (σ : SignatureMorphism A B) (τ : SignatureMorphism B C)
             (Γ : Ctx A) (w : list (Sorts A)) (ts : HVec (Term A Γ) w),
               map_on_terms (comp_FOSig τ σ) ts =
                 rew [λ Γ, HVec (Term C Γ) _] (map_map σ τ Γ) in
                   rew map_map σ τ w in map_on_terms τ (map_on_terms σ ts)).
      { intros. rewrite H0. unfold on_terms_obligation_1. cbn. unfold comp_FOSig_obligation_1.
        simplify_eqs. destruct eqH. destruct eqH3. cbn. unfold on_terms_obligation_2.
        simplify_eqs. destruct eqH1. cbn. destruct eqH0. cbn. f_equal. destruct eqH2. cbn.
        simplify_eqs. auto. }
      intros. induction ts; cbn.
      + now simplify_eqs.
      + rewrite IHts; cbn.
        rewrite <- on_terms_comp.
        simplify_eqs. destruct eqH; cbn.
        now simplify_eqs.
Qed.

Lemma map_on_terms_comp {A B C : Signature}
      (σ : SignatureMorphism A B) (τ : SignatureMorphism B C)
      {Γ : Ctx A} {w : list (Sorts A)} (ts : HVec (Term A Γ) w) :
      map_on_terms (comp_FOSig τ σ) ts =
        rew [λ Γ, HVec (Term C Γ) _] (map_map σ τ Γ) in
          rew (map_map σ τ w) in
            (map_on_terms τ (map_on_terms σ ts)).
Proof.
  induction ts; cbn.
  - now simplify_eqs.
  - rewrite IHts; cbn.
    rewrite <- on_terms_comp.
    rewrite map_map_cons_pfs.
    rewrite <- rew_map.
    now simplify_eqs.
Qed.

Equations? fmap_FOPEQ {A B : FOSig} {Γ : Ctx A} (σ : A ~{ FOSig }~> B) :
    FOPEQ A Γ ~{ SetCat }~> FOPEQ B (map σ Γ) :=
  fmap_FOPEQ σ (Forall ψ   ) := Forall (fmap_FOPEQ σ ψ) ;
  fmap_FOPEQ σ (Exists ψ   ) := Exists (fmap_FOPEQ σ ψ) ;
  fmap_FOPEQ σ (Pred P args) := Pred (on_preds σ P) _ ;
  fmap_FOPEQ σ (And α β    ) := And (fmap_FOPEQ σ α) (fmap_FOPEQ σ β) ;
  fmap_FOPEQ σ (Or α β     ) := Or (fmap_FOPEQ σ α) (fmap_FOPEQ σ β) ;
  fmap_FOPEQ σ (Imp α β    ) := Imp (fmap_FOPEQ σ α) (fmap_FOPEQ σ β) ;
  fmap_FOPEQ σ (Not ψ      ) := Not (fmap_FOPEQ σ ψ) ;
  fmap_FOPEQ σ (Equal t₁ t₂) := Equal (on_terms σ t₁) (on_terms σ t₂) ;
  fmap_FOPEQ σ (FOL_T      ) := FOL_T ;
  fmap_FOPEQ σ (FOL_F      ) := FOL_F .

  - refine (rew _ in map_on_terms σ args).
    now rewrite tagged_morphism_commutes.
Defined.

Global Transparent fmap_FOPEQ.

Theorem fmap_id_FOSen : ∀ (Σ : Signature) {Γ : Ctx Σ} (φ : FOPEQ Σ Γ),
  fmap_FOPEQ (id_FOSig Σ) φ = rew [FOPEQ Σ] (map_id Γ)^ in φ.
Proof.
  induction φ; cbn in * |- *.
  - rewrite map_id_cons_pfs in IHφ.
    rewrite <- ap_V in IHφ.
    rewrite IHφ.
    rewrite <- rew_map.
    rewrite <- (lemma2_3_11a (FOPEQ Σ) (cons s) (λ _, Forall)).
    reflexivity.
  - rewrite map_id_cons_pfs in IHφ.
    rewrite <- ap_V in IHφ.
    rewrite IHφ.
    rewrite <- rew_map.
    rewrite <- (lemma2_3_11a (FOPEQ Σ) (cons s) (λ _, Exists)).
    reflexivity.
  - repeat rewrite on_terms_id. now simplify_eqs.
  - unfold fmap_FOPEQ_obligation_1. repeat rewrite map_on_terms_id. simplify_eqs.
    rewrite rew_compose. now simplify_eqs.
  - rewrite IHφ1, IHφ2. now case (map_id Γ)^.
  - rewrite IHφ1, IHφ2. now case (map_id Γ)^.
  - rewrite IHφ1, IHφ2. now case (map_id Γ)^.
  - rewrite IHφ. now case (map_id Γ)^.
  - now simplify_eqs.
  - now simplify_eqs.
Qed.

Theorem fmap_compose_FOSen :
  ∀ {A B C : FOSig} (f : B ~> C) (g : A ~> B)
    {Γ : Ctx A} (φ : FOPEQ A Γ),
  fmap_FOPEQ (comp_FOSig f g) φ =
    rew map_map g f Γ in fmap_FOPEQ f (fmap_FOPEQ g φ).
Proof.
  induction φ; cbn in * |- *; auto.
  - rewrite IHφ; cbn in *.
    rewrite map_map_cons_pfs.
    rewrite <- (rew_map _ (cons (f (g s)))).
    now rewrite (map_subst (λ _, Forall)).
  - rewrite map_map_cons_pfs in IHφ.
    rewrite IHφ.
    rewrite <- (rew_map _ (cons (f (g s)))).
    now rewrite (map_subst (λ _, Exists)).
  - repeat rewrite <- on_terms_comp.
    now destruct (map_map g f Γ).
  - unfold fmap_FOPEQ_obligation_1. cbn.
    unfold comp_FOSig_obligation_2.
    simplify_eqs.
    induction h.
    * cbn in *. destruct eqH0. cbn.
      f_equal. destruct eqH1. cbn.
      destruct eqH2. cbn. now simplify_eqs.
    * rewrite map_on_terms_comp; cbn in *.
      rewrite map_map_cons_pfs.
      rewrite <- rew_map. destruct eqH2.
      simplify_eqs.
      destruct eqH2. cbn.
      case eqH0. cbn. simplify_eqs. auto.
  - rewrite IHφ1, IHφ2. now simplify_eqs.
  - rewrite IHφ1, IHφ2. now simplify_eqs.
  - rewrite IHφ1, IHφ2. now simplify_eqs.
  - rewrite IHφ. now simplify_eqs.
  - now simplify_eqs.
  - now simplify_eqs.
Qed.

Definition FOSen : FOSig ⟶ SetCat.
  refine {|
    fobj := λ Σ : FOSig, FOPEQ Σ [] : SetCat ;
    fmap := λ A B, @fmap_FOPEQ A B [] ;
  |}; repeat intro.
  - rewrite fmap_id_FOSen. now simplify_eqs.
  - rewrite fmap_compose_FOSen. now simplify_eqs.
Defined.

Lemma helper_eval_term_reduct
    (Σ Σ' : Signature) (A' : Algebra Σ')
    (σ : SignatureMorphism Σ Σ')
    {Γ s} (t : Term Σ Γ s) env :
  eval_term (ReductAlgebra σ A') t env =
    eval_term A' (on_terms σ t) (reindex σ env).
Proof.
  - induction t using term_ind'.
    + cbn in *.
      induction m; cbn in *.
      * now rewrite (hvec_cons env).
      * rewrite (hvec_cons env); cbn; congruence.
    + simp on_terms eval_term; cbn.
      repeat rewrite map_eval_term_hmap.
      rewrite map_on_terms_hmap.
      unfold Algebra.ReductAlgebra_obligation_2, Algebra.ReductAlgebra_obligation_1, on_terms_obligation_1.
      simplify_eqs. destruct eqH. simpl eq_rect.
      simp eval_term. f_equal. destruct eqH0. cbn.
      rewrite map_eval_term_hmap.
      rewrite hmap_reindex.
      rewrite <- hmap_hmap.
      now setoid_rewrite (proj1 (map_ext_HForall _ _ _) H).
Qed.

Lemma helper_map_eval_term_reduct
    (Σ Σ' : Signature) (A' : Algebra Σ')
    (σ : SignatureMorphism Σ Σ')
    [Γ w] (args : HVec (Term Σ Γ) w) env :
  map_eval_term A' (map_on_terms σ args) (reindex σ env) =
    reindex σ (map_eval_term (ReductAlgebra σ A') args env).
Proof.
  induction args.
  - reflexivity.
  - cbn. f_equal.
    * symmetry; apply helper_eval_term_reduct.
    * apply IHargs.
Qed.

(*****************************************************************************)
(** * First-Order Model Functor *)

Definition AlgebraHom [Σ] (A B : Algebra Σ) :=
  { h | AlgHom A B h }.

Lemma eq_alghom [Σ] (A B : Algebra Σ) (f g : AlgebraHom A B)
  (p : `f = `g) : f = g.
Proof.
  destruct f, g; cbn in p.
  assert (rew p in a = a0).
  - apply proof_irrelevance.
  - now simplify_eqs.
Qed.

Definition id_alghom [Σ] (A : Algebra Σ) : AlgebraHom A A.
  exists (λ _, idmap).
  repeat intro; rewrite hmap_id; auto.
Defined.

Definition comp_alghom [Σ] (A B C : Algebra Σ)
  (f : AlgebraHom B C) (g : AlgebraHom A B) : AlgebraHom A C.
Proof.
  exists (λ s x, `f s (`g s x)).
  repeat intro; rewrite hmap_hmap, (proj2_sig g), (proj2_sig f); auto.
Defined.

Program Instance Alg Σ : Category := {|
  obj := Algebra Σ ;
  hom := λ A B, AlgebraHom A B ;
  homset := Morphism_equality ;
  Category.id := λ A, id_alghom A ;
  compose := λ A B C, comp_alghom A B C ;
|}.
Next Obligation. refine (eq_alghom _ _ _ _ _); reflexivity. Qed.
Next Obligation. refine (eq_alghom _ _ _ _ _); reflexivity. Qed.
Next Obligation. refine (eq_alghom _ _ _ _ _); reflexivity. Qed.
Next Obligation. refine (eq_alghom _ _ _ _ _); reflexivity. Qed.

Lemma reindex_hmap
    [I J] [A B : I -> Type]
    (f : J -> I) (h : ∀ s, A s -> B s)
    [w] (l : HVec (A ∘ f) w) :
  hmap h (reindex f l) = reindex f (hmap (h ∘ f) l).
Proof.
  induction l; cbn in *; f_equal; auto.
Qed.

Program Instance ReductFunctor
    [Σ Σ' : FOSig] (σ : Σ ~> Σ') : Alg Σ' ⟶ Alg Σ := {|
  fobj := ReductAlgebra σ ;
  fmap := λ A B h, exist _ (h ∘ σ) _ ;
|}.
Next Obligation.
  simpl interp_funcs. unfold Algebra.ReductAlgebra_obligation_2, Algebra.ReductAlgebra_obligation_1.
  simplify_eqs.
  refine (eq_trans _ _).
  rewrite (proj2_sig h); auto.
  rewrite <- reindex_hmap. f_equal.
  now destruct eqH.
Defined.
Next Obligation. refine (eq_alghom _ _ _ _ _); reflexivity. Defined.
Next Obligation. refine (eq_alghom _ _ _ _ _); reflexivity. Defined.

Lemma reduct_id (Σ : Signature) (A : Algebra Σ) :
  ReductAlgebra (id_FOSig Σ) A = A.
Proof.
  unfold ReductAlgebra; destruct A.
  cbn. repeat change (λ x, ?f x) with f. f_equal.
  - funext F args.
    rewrite reindex_id.
    rewrite rew_compose.
    now simplify_eqs.
  - funext P args.
    rewrite reindex_id.
    rewrite rew_compose.
    now simplify_eqs.
Qed.

Lemma reduct_comp {A B C : FOSig} (g : B ~> C) (f : A ~> B) (M : Algebra C) :
  ReductAlgebra (comp_FOSig g f) M = ReductAlgebra f (ReductAlgebra g M).
Proof.
  destruct M; unfold ReductAlgebra; cbn; f_equal.
  - funext F args.
    rewrite <- reindex_comp.
    rewrite (rew_map _ _ (Algebra.ReductAlgebra_obligation_2 A B f F)).
    repeat rewrite rew_compose.
    simplify_eqs. destruct eqH. cbn.
    f_equal. destruct eqH0, eqH2. cbn.
    now simplify_eqs.
  - funext P args.
    rewrite <- reindex_comp.
    rewrite rew_compose.
    simplify_eqs.
    destruct eqH1. cbn.
    now simplify_eqs.
Qed.

Definition FOPEQ_Mod : FOSig ⟶ Cat^op := {|
  fobj := Alg : FOSig -> Cat^op ;
  fmap := ReductFunctor ;
  fmap_id := reduct_id ;
  fmap_comp := @reduct_comp ;
|}.

(*****************************************************************************)
(** * Satisfaction for First-Order Logic *)

Theorem FOPEQ_satisfaction_with_context :
  ∀ (Σ Σ' : Signature) (σ : SignatureMorphism Σ Σ')
    {Γ : Ctx Σ} (φ : FOPEQ Σ Γ)
    (A' : Algebra Σ') (env : HVec (interp_sorts A' ∘ σ) Γ),
  interp_fopeq A' (fmap_FOPEQ σ φ) (reindex σ env) <->
    interp_fopeq (ReductAlgebra σ A') φ env.
Proof.
  intros; induction φ; cbn; split; auto.
  - intros.
    pose proof (H' := H x).
    pose (env' := x ::: reindex σ env).
    change (σ s :: map σ Γ) with (map σ (s :: Γ)) in env'.
    pose proof (IHφ' := IHφ (reindex' σ env')).
    destruct IHφ' as [IHφ_right _].
    rewrite (reindex_reindex'_id σ env') in IHφ_right.
    unfold env' in IHφ_right; cbn in IHφ_right.
    rewrite (reindex'_reindex_id σ env) in IHφ_right.
    exact (IHφ_right H').
  - intros.
    pose proof (H' := H x).
    pose (env' := x ::: reindex σ env).
    change (σ s :: map σ Γ) with (map σ (s :: Γ)) in env'.
    pose proof (IHφ' := IHφ (reindex' σ env')).
    destruct IHφ' as [_ IHφ_left].
    rewrite (reindex_reindex'_id σ env') in IHφ_left.
    unfold env' in IHφ_left; cbn in IHφ_left.
    rewrite reindex'_reindex_id in IHφ_left.
    exact (IHφ_left H').
  - intros. destruct H.
    exists x.
    pose (env' := x ::: reindex σ env).
    change (σ s :: map σ Γ) with (map σ (s :: Γ)) in env'.
    pose proof (IHφ' := IHφ (reindex' σ env')).
    rewrite (reindex_reindex'_id σ env') in IHφ'.
    destruct IHφ' as [IHφ_right _].
    pose proof (i := IHφ_right H).
    unfold env' in i.
    cbn in i.
    rewrite (reindex'_reindex_id σ env) in i.
    exact i.
  - intros. destruct H.
    exists x.
    pose (env' := x ::: reindex σ env).
    change (σ s :: map σ Γ) with (map σ (s :: Γ)) in env'.
    pose (IHφ' := IHφ (reindex' σ env')).
    rewrite (reindex_reindex'_id σ env') in IHφ'.
    destruct IHφ' as [_ IHφ_left].
    unfold env' in IHφ_left; cbn in IHφ_left.
    rewrite reindex'_reindex_id in IHφ_left.
    pose (i := IHφ_left H).
    exact i.
  - intros. do 2 rewrite -> helper_eval_term_reduct. apply H.
  - intros. do 2 rewrite <- helper_eval_term_reduct. apply H.
  - unfold fmap_FOPEQ_obligation_1, Algebra.ReductAlgebra_obligation_3.
    rewrite <- helper_map_eval_term_reduct.
    simplify_eqs.
    cut (interp_preds A' (on_preds σ P)
    (map_eval_term A' (rew [HVec (Term Σ' (map σ Γ))] eqH in map_on_terms σ h)
       (reindex σ env)) = interp_preds A' (on_preds σ P)
       (rew [HVec A'] eqH in map_eval_term A' (map_on_terms σ h) (reindex σ env))).
    { intros. change (λ x, ?f x) with f in *. rewrite <- H. auto. }
    f_equal. now destruct eqH.
  - unfold fmap_FOPEQ_obligation_1, Algebra.ReductAlgebra_obligation_3.
    rewrite <- helper_map_eval_term_reduct.
    simplify_eqs.
    cut (interp_preds A' (on_preds σ P)
    (map_eval_term A' (rew [HVec (Term Σ' (map σ Γ))] eqH in map_on_terms σ h)
      (reindex σ env)) = interp_preds A' (on_preds σ P)
      (rew [HVec A'] eqH in map_eval_term A' (map_on_terms σ h) (reindex σ env))).
    { intros. change (λ x, ?f x) with f in *. rewrite H. auto. }
    f_equal. now destruct eqH.
  - intros H.
    destruct H as [H1 H2].
    exact (conj (proj1 (IHφ1 env) H1) (proj1 (IHφ2 env) H2)).
  - intros H.
    destruct H as [H1 H2].
    exact (conj (proj2 (IHφ1 env) H1) (proj2 (IHφ2 env) H2)).
  - intros H. destruct H.
    * left. exact (proj1 (IHφ1 env) H).
    * right. exact (proj1 (IHφ2 env) H).
  - intros H. destruct H.
    * left. exact (proj2 (IHφ1 env) H).
    * right. exact (proj2 (IHφ2 env) H).
  - intros H.
    exact (proj1 (IHφ2 env) ∘ H ∘ proj2 (IHφ1 env)).
  - intros H.
    exact (proj2 (IHφ2 env) ∘ H ∘ proj1 (IHφ1 env)).
  - intros H φ'.
    pose proof (H' := proj2 (IHφ env) φ').
    contradiction.
  - intros H φ'.
    pose proof (H' := proj1 (IHφ env) φ').
    contradiction.
Qed.

Definition FOPEQ_satisfaction
    (Σ Σ' : FOSig) (σ : Σ ~> Σ') (φ : FOPEQ Σ []) (A' : Algebra Σ') :=
  FOPEQ_satisfaction_with_context (Γ := []) Σ Σ' σ φ A' ⟨⟩.

Require Import Category.Functor.Opposite.

Definition INS_FOPEQ : Institution := {|
  Sig := FOSig ;
  Sen := FOSen ;
  Mod := FOPEQ_Mod^op ;
  interp := λ _ A φ, interp_fopeq A φ ⟨⟩ ;
  sat := FOPEQ_satisfaction ;
|}.

(******************************************************************************)
(** * Entailment systems *)
Section EntailmentSystems.
Context {I : Institution}.

Class EntailmentRelClass (R : ∀ Σ : Sig[I], list (Sen[I] Σ) -> Sen[I] Σ -> Prop) := {
  entailment_axiom_1 : ∀ Σ E φ, In φ E -> R Σ E φ ;
  entailment_axiom_2 : ∀ Σ E Γ φ,
    List.Forall (R Σ E) Γ -> R Σ Γ φ -> R Σ E φ ;
  entailment_axiom_3 : ∀ (Σ Σ' : Sig[I]) (σ : Σ ~> Σ') E φ,
    R Σ E φ -> R Σ' (map (fmap[Sen] σ) E) (fmap[Sen] σ φ)
}.

End EntailmentSystems.

Generalizable All Variables.

Reserved Notation "E ⊢ φ" (at level 90).

(** This is a bit of a homebrew; just for testing. *)
Inductive FOPEQ_entails A {G} : list (FOPEQ A G) -> list (FOPEQ A G) -> Prop :=
| triviality  : ∀ Γ, Γ ⊢ []
| top_R       : ∀ Γ Δ, Γ ⊢ FOL_T :: Δ
| bot_L       : ∀ Γ Δ, FOL_F :: Γ ⊢ Δ
| hypothesis  : ∀ Γ Δ a, a :: Γ ⊢ a :: Δ
| reorder_hyp : ∀ Γ Δ a b, a :: b :: Γ ⊢ Δ -> b :: a :: Γ ⊢ Δ
| cycle_hyp   : ∀ Γ Δ a, Γ ++ [a] ⊢ Δ -> a :: Γ ⊢ Δ
| weakening   : ∀ Γ Δ a, Γ ⊢ Δ -> a :: Γ ⊢ Δ
| contr_l     : ∀ Γ Δ a, a :: a :: Γ ⊢ Δ -> a :: Γ ⊢ Δ
| contr_r     : ∀ Γ Δ a, Γ ⊢ a :: a :: Δ -> Γ ⊢ a :: Δ
| bigcontr    : ∀ Γ Δ, Γ ++ Γ ⊢ Δ -> Γ ⊢ Δ
| cut_rule    : ∀ Γ Σ Δ Π a, Γ ⊢ a :: Δ -> a :: Σ ⊢ Π -> Γ ++ Σ ⊢ Δ ++ Π

| imp_l  : ∀ Γ Σ Δ Π a b, Γ ⊢ a :: Δ -> b :: Σ ⊢ Π -> Imp a b :: Γ ++ Σ ⊢ Δ ++ Π
| imp_r  : ∀ Γ Δ a b, a :: Γ ⊢ b :: Δ -> Γ ⊢ Imp a b :: Δ
| and_l1  : ∀ Γ Δ a b, a :: Γ ⊢ Δ -> And a b :: Γ ⊢ Δ
| and_l2  : ∀ Γ Δ a b, b :: Γ ⊢ Δ -> And a b :: Γ ⊢ Δ
| and_r  : ∀ Γ Σ Δ Π a b, Γ ⊢ a :: Δ -> Σ ⊢ b :: Π -> Γ ++ Σ ⊢ And a b :: Δ ++ Π
| and_e1 : ∀ Γ Δ a b, Γ ⊢ And a b :: Δ -> Γ ⊢ a :: Δ
| and_e2 : ∀ Γ Δ a b, Γ ⊢ And a b :: Δ -> Γ ⊢ b :: Δ

| or_l   : ∀ Γ Σ Δ Π a b, a :: Γ ⊢ Δ -> b :: Σ ⊢ Π -> Or a b :: Γ ++ Σ ⊢ Δ ++ Π
| or_r1  : ∀ Γ Δ a b, Γ ⊢ a :: Δ -> Γ ⊢ Or a b :: Δ
| or_r2  : ∀ Γ Δ a b, Γ ⊢ b :: Δ -> Γ ⊢ Or a b :: Δ
| or_e   : ∀ Γ Δ a b c, Γ ⊢ Or a b :: Δ -> a :: Γ ⊢ c :: Δ -> b :: Γ ⊢ c :: Δ -> Γ ⊢ c :: Δ
    where "Γ ⊢ φ" := (FOPEQ_entails _ Γ φ).

(* follows by repeated application of the weakening rule *)
Lemma axiom_holds_in_any_context `(E : list (FOSen Σ)) (p : FOSen Σ) :
  [] ⊢ [p] -> E ⊢ [p].
Proof.
  intros H; induction E.
  - assumption.
  - apply weakening.
    exact IHE.
Qed.

Lemma example_deduction1 Σ (A B : FOSen Σ) :
  [] ⊢ [Imp A (Imp B A)].
Proof. eauto using FOPEQ_entails. Qed.

Lemma example_deduction2 Σ (A B : FOSen Σ) :
  [] ⊢ [And (Imp A (Or A B)) (Imp B (Or A B))].
Proof.
  (* change ([] : list (FOPEQ _ _)) with ([] ++ []). *)
  change (?l ⊢ ?r) with (l ++ [] ⊢ r ++ []).
  apply and_r.
  - apply imp_r.
    apply or_r1.
    apply hypothesis.
  - apply imp_r.
    apply or_r2.
    apply hypothesis.
Qed.

Lemma example_deduction3 Σ (A B C : FOSen Σ) :
  [] ⊢ [Imp (Imp A C) (Imp (Imp B C) (Imp (Or A B) C))].
Proof.
  repeat apply imp_r.
  change (?l ⊢ ?r) with (l ++ [] ⊢ r ++ []).
  apply or_l.
  - apply cycle_hyp, cycle_hyp; cbn.
    change (?l ⊢ ?r) with (l ++ [] ⊢ r ++ []).
    apply imp_l.
    * change (?l ⊢ ?r) with (l ++ [] ⊢ r ++ []).
      apply hypothesis.
    * apply triviality.
  - apply triviality.
Qed.

Lemma example_deduction4 Σ (A B : FOSen Σ) :
  [] ⊢ [Imp (And A B) (And B A)].
Proof.
  apply imp_r.
  apply contr_l.
  change (?l ⊢ ?r) with (l ⊢ r ++ []).
  change ([And A B; And A B]) with ([And A B] ++ [And A B]).
  apply and_r.
  - apply and_l2, hypothesis.
  - apply and_l1, hypothesis.
Qed.

Lemma entailment_helper `(E1 : list (FOPEQ Σ Γ)) E2 :
  List.Forall (λ ψ, E1 ⊢ [ψ]) E2 <-> E1 ⊢ [fold_right And FOL_T E2].
Proof.
  split; intros.
  - induction E2.
    * cbn in *. apply top_R.
    * cbn in *.
      apply bigcontr.
      change (?l ⊢ ?r) with (l ⊢ r ++ []).
      apply and_r.
      + now apply Forall_inv in H.
      + apply IHE2.
        now apply Forall_inv_tail in H.
  - induction E2.
    * easy.
    * cbn in *.
      pose proof (and_e1 _ _ _ _ _ H).
      pose proof (and_e2 _ _ _ _ _ H).
      apply Forall_cons; auto.
Qed.

Lemma is_entailment_system_FOPEQ_with_context :
  ∀ (Σ Σ' : Sig[INS_FOPEQ])
    (σ : Σ ~> Σ')
    (Γ : Ctx Σ)
    (E : list (FOPEQ Σ Γ))
    (φ : FOPEQ Σ Γ)
    (H : E ⊢ [φ]),
  map (fmap_FOPEQ σ) E ⊢ [fmap_FOPEQ σ φ].
Proof.
  intros.
  induction φ; intros.
  - admit. (* need rules for quantifiers *)
  - admit. (* need rules for quantifiers *)
  - cbn in *. admit. (* need rules for equality *)
  - cbn. admit. (* need rules for predicates *)
  - cbn in *.
    apply bigcontr.
    change [And (fmap_FOPEQ σ φ1) (fmap_FOPEQ σ φ2)] with ([And (fmap_FOPEQ σ φ1) (fmap_FOPEQ σ φ2)] ++ []).
    apply and_r; [apply IHφ1 | apply IHφ2]; [ apply and_e1 in H | apply and_e2 in H ]; trivial.
  - cbn in *. epose proof (or_e _ _ _ _ _ _ H).
  all: admit.
Admitted.

Theorem is_entailment_system_FOPEQ : EntailmentRelClass (I := INS_FOPEQ) (λ _ E ψ, E ⊢ [ψ]).
  refine {|
    entailment_axiom_1 := _ ;
    entailment_axiom_2 := _ ;
    entailment_axiom_3 := _ ;
  |}; intros.
  - induction E; intros.
    * contradiction.
    * cbn in *. destruct H.
      + rewrite H. apply hypothesis.
      + apply weakening.
        exact (IHE H).
  - induction Γ; intros.
    * apply axiom_holds_in_any_context. assumption.
    * apply (IHΓ (Forall_inv_tail H)).
      (* pose proof (IHΓ a (Forall_inv_tail H)). *)
      pose proof (Forall_inv H). cbn in H1.
      pose proof (Forall_inv_tail H).
      apply entailment_helper in H2.
      admit.
  - now apply (is_entailment_system_FOPEQ_with_context _ _ _ []).
Admitted.

author: ConorReynolds

repo: coq-institutions


text:
Set Warnings "-notation-overridden,-parsing".
From LF Require Export Logic.
Require Coq.omega.Omega.

Inductive even : nat -> Prop :=
  | ev_0 : even 0
  | ev_SS : forall n, even n -> even (S (S n)).

Theorem ev_4 : even 4.
Proof. apply ev_SS. apply ev_SS. apply ev_0. Qed.

Theorem ev_4' : even 4.
Proof. apply (ev_SS 2 (ev_SS 0 ev_0)). Qed.

Theorem ev_plus4 : forall n, even n -> even (4 + n).
Proof.
  intros n. simpl. intros Hn.
  apply ev_SS. apply ev_SS. apply Hn.
Qed.

Theorem ev_double : forall n,
  even (double n).
Proof.
  intros. induction n.
  - simpl. apply ev_0.
  - simpl. apply ev_SS. apply IHn.
Qed.

Print even.

(*不再对n分类讨论，而是对假设分类讨论。此时假设已经具备了构造子*)
(*2019.7.20*)
Theorem ev_inversion :
  forall (n : nat), even n ->
    (n = 0) \/ (exists n', n = S (S n') /\ even n').
Proof.
  intros n E.
  destruct E as [ | n' E'].
  - (* E = ev_0 : even 0 *)
    left. reflexivity.
  - (* E = ev_SS n' E' : even (S (S n')) *)
    right. exists n'. split. reflexivity. apply E'.
Qed.

Theorem ev_minus2 : forall n,
  even n -> even (pred (pred n)).
Proof.
  intros n E.
  destruct E as [| n' E'].
  - (* E = ev_0 *) simpl. apply ev_0.
  - (* E = ev_SS n' E' *) simpl. apply E'.
Qed.

Theorem evSS_ev : forall n, even (S (S n)) -> even n.
Proof. intros n H. apply ev_inversion in H. destruct H.
 - discriminate H.
 - destruct H as [n' [Hnm Hev]]. injection Hnm.
   intro Heq. rewrite Heq. apply Hev.
Qed.

Theorem evSS_ev' : forall n,
  even (S (S n)) -> even n.
Proof.
  intros n E.
  inversion E as [| n' E'].
  (* We are in the E = ev_SS n' E' case now. *)
  apply E'.
Qed.

Theorem one_not_even : ~ even 1.
Proof.
  intros H. apply ev_inversion in H.
  destruct H as [ | [m [Hm _]]].
  - discriminate H.
  - discriminate Hm.
Qed.
Theorem one_not_even' : ~ even 1.
  intros H. inversion H.
Qed.

Theorem SSSSev__even : forall n,
  even (S (S (S (S n)))) -> even n.
Proof.
  intros. inversion H. inversion H1. apply H3.
Qed.

Theorem even5_nonsense :
  even 5 -> 2 + 2 = 9.
Proof.
  intros.
  inversion H. inversion H1. inversion H3.
Qed.

Theorem inversion_ex1 : forall (n m o : nat),
  [n; m] = [o; o] ->
  [n] = [m].
Proof.
  intros n m o H. inversion H. reflexivity. Qed.

Theorem inversion_ex2 : forall (n : nat),
  S n = O ->
  2 + 2 = 5.
Proof.
  intros n contra. inversion contra. Qed.

Lemma ev_even_firsttry : forall n,
  even n -> exists k, n = double k.
Proof.
  intros n E. inversion E as [|n' E'].
  - exists 0. reflexivity.
  - simpl.
    assert (I : (exists k', n' = double k') ->
                (exists k, S (S n') = double k)).
    { intros [k' Hk']. rewrite Hk'. exists (S k'). reflexivity. }
    apply I.
Abort.

Lemma ev_even : forall n,
  even n -> exists k, n = double k.
Proof.
  intros n E.
  induction E as [|n' E' IH].
  - (* E = ev_0 *)
    exists 0. reflexivity.
  - (* E = ev_SS n' E'
       同时 IH : exists k', n' = double k' *)
    destruct IH as [k' Hk'].
    rewrite Hk'. exists (S k'). reflexivity.
Qed.

Theorem ev_even_iff : forall n,
  even n <-> exists k, n = double k.
Proof.
  intros n. split.
  - (* -> *) apply ev_even.
  - (* <- *) intros [k Hk]. rewrite Hk. apply ev_double.
Qed.

Theorem ev_sum : forall n m, even n -> even m -> even (n + m).
Proof.
  intros. induction H.
  - simpl. apply H0.
  - simpl. apply ev_SS. apply IHeven.
Qed.

Inductive even' : nat -> Prop :=
| even'_0 : even' 0
| even'_2 : even' 2
| even'_sum n m (Hn : even' n) (Hm : even' m) : even' (n + m).

Lemma SSn_lemma : forall n: nat, S(S n) = n+2.
Proof.
  intros. simpl. induction n. apply plus_O_n. rewrite IHn. simpl. reflexivity.
Qed.

Theorem even'_ev : forall n, even' n <-> even n.
Proof.
  split.
  - intros. induction H.
    + apply ev_0.
    + apply ev_SS. apply ev_0.
    + apply ev_sum.
      * apply IHeven'1.
      * apply IHeven'2.
  - intros. induction H.
    + apply even'_0.
    + rewrite SSn_lemma. apply even'_sum.
      * apply IHeven.
      * apply even'_2.
Qed.

Theorem ev_ev__ev : forall n m,
  even (n+m) -> even n -> even m.
Proof.
  intros. induction H0.
  simpl in H.
  - apply H.
  - simpl in H. inversion H. apply IHeven in H2. apply H2.
Qed.

Theorem ev_plus_plus : forall n m p,
  even (n+m) -> even (n+p) -> even (m+p).
Proof.
Admitted.

Module Playground.

Inductive le : nat -> nat -> Prop :=
  | le_n n : le n n
  | le_S n m (H : le n m) : le n (S m).
Notation "m <= n" := (le m n).

Theorem test_le1 :
  3 <= 3.
Proof.
  (* 课上已完成 *)
  apply le_n. Qed.
Theorem test_le2 :
  3 <= 6.
Proof.
  (* 课上已完成 *)
  apply le_S. apply le_S. apply le_S. apply le_n. Qed.
Theorem test_le3 :
  (2 <= 1) -> 2 + 2 = 5.
Proof.
  (* 课上已完成 *)
  intros H. inversion H. inversion H2. Qed.

End Playground.
Definition lt (n m:nat) := le (S n) m.
Notation "m < n" := (lt m n).

Inductive square_of : nat -> nat -> Prop :=
  | sq n : square_of n (n * n).
Inductive next_nat : nat -> nat -> Prop :=
  | nn n : next_nat n (S n).
Inductive next_even : nat -> nat -> Prop :=
  | ne_1 n : even (S n) -> next_even n (S n)
  | ne_2 n (H : even (S (S n))) : next_even n (S (S n)).

Lemma le_trans : forall m n o, m <= n -> n <= o -> m <= o.
Proof.
  intros.
  generalize dependent H.
  generalize dependent m.
  induction H0.
  - intros. apply H.
  - intros. apply le_S. apply IHle. apply H.
Qed.

Theorem O_le_n : forall n,
  0 <= n.
Proof.
  intros. induction n.
  - apply le_n.
  - apply le_S. apply IHn.
Qed.

Theorem n_le_m__Sn_le_Sm : forall n m,
  n <= m -> S n <= S m.
Proof.
  intros. induction H.
  - apply le_n.
  - apply le_S. apply IHle.
Qed.

Theorem Sn_le_Sm__n_le_m : forall n m,
  S n <= S m -> n <= m.
Proof.
  intros.
  inversion H.
  - apply le_n.
  - apply le_trans with (n := S n). (*m>=Sn>=n*)
    * apply le_S. apply le_n.
    * apply H1.
Qed.

Theorem le_plus_l : forall a b,
  a <= a + b.
Proof.
  intros. induction a.
  - simpl. apply O_le_n.
  - simpl. apply n_le_m__Sn_le_Sm. apply IHa.
Qed.

Theorem plus_lt : forall n1 n2 m,
  n1 + n2 < m ->
  n1 < m /\ n2 < m.
Proof.
  intros. unfold lt. unfold lt in H. induction H.
  - split.
    + apply n_le_m__Sn_le_Sm. apply le_plus_l.
    + apply n_le_m__Sn_le_Sm. rewrite plus_comm. apply le_plus_l.
  - split. destruct IHle.
    + apply le_trans with (n:= m).
      * apply H0.
      * apply le_S. apply le_n.
    + apply le_trans with (n:= m).
      * destruct IHle. apply H1.
      * apply le_S. apply le_n.
Qed.

Theorem lt_S : forall n m,
  n < m ->
  n < S m.
Proof.
  intros. apply le_trans with (o:= S m) in H.
  + unfold lt. apply H.
  + apply le_S. apply le_n.
Qed.

Theorem leb_complete : forall n m,
  n <=? m = true -> n <= m.
Proof.
  intros. induction n.
  - apply O_le_n.
  - simpl in H. induction m.
    + discriminate.
    + apply n_le_m__Sn_le_Sm. Admitted.

Theorem leb_correct : forall n m,
  n <= m ->
  n <=? m = true.
Proof.
  intros. induction m.
  - Admitted.

Theorem leb_true_trans : forall n m o,
  n <=? m = true -> m <=? o = true -> n <=? o = true.
Proof.
  (* 请在此处解答 *) Admitted.

Theorem leb_iff : forall n m,
  n <=? m = true <-> n <= m.
Proof.
  split.
  - intros. apply leb_complete in H. apply H.
  - intros. apply leb_correct. apply H.
Qed.
(*
Inductive subseq : list nat -> list nat -> Prop :=
  | subseq_nil : subseq [] l
  | subseq_n n : subseq n n

Theorem subseq_refl : forall (l : list nat), subseq l l.
Proof.
  (* 请在此处解答 *) Admitted.
Theorem subseq_app : forall (l1 l2 l3 : list nat),
  subseq l1 l2 ->
  subseq l1 (l2 ++ l3).
Proof.
  (* 请在此处解答 *) Admitted.
Theorem subseq_trans : forall (l1 l2 l3 : list nat),
  subseq l1 l2 ->
  subseq l2 l3 ->
  subseq l1 l3.
Proof.
  (* 请在此处解答 *) Admitted.
 *)

Inductive reg_exp {T : Type} : Type :=
  | EmptySet
  | EmptyStr
  | Char (t : T)
  | App (r1 r2 : reg_exp)
  | Union (r1 r2 : reg_exp)
  | Star (r : reg_exp).

Inductive exp_match {T} : list T -> reg_exp -> Prop :=
  | MEmpty : exp_match [] EmptyStr
  | MChar x : exp_match [x] (Char x)
  | MApp s1 re1 s2 re2
             (H1 : exp_match s1 re1)
             (H2 : exp_match s2 re2) :
             exp_match (s1 ++ s2) (App re1 re2)
  | MUnionL s1 re1 re2
                (H1 : exp_match s1 re1) :
                exp_match s1 (Union re1 re2)
  | MUnionR re1 s2 re2
                (H2 : exp_match s2 re2) :
                exp_match s2 (Union re1 re2)
  | MStar0 re : exp_match [] (Star re)
  | MStarApp s1 s2 re
                 (H1 : exp_match s1 re)
                 (H2 : exp_match s2 (Star re)) :
                 exp_match (s1 ++ s2) (Star re).

Notation "s =~ re" := (exp_match s re) (at level 80).

Example reg_exp_ex1 : [1] =~ Char 1.
Proof.
  apply MChar.
Qed.

Example reg_exp_ex2 : [1; 2] =~ App (Char 1) (Char 2).
Proof.
  apply (MApp [1] _ [2]).
  - apply MChar.
  - apply MChar.
Qed.

Example reg_exp_ex3 : ~([1; 2] =~ Char 1).
Proof.
  intros H. inversion H.
Qed.

Fixpoint reg_exp_of_list {T} (l : list T) :=
  match l with
  | [] => EmptyStr
  | x :: l' => App (Char x) (reg_exp_of_list l')
  end.
Example reg_exp_ex4 : [1; 2; 3] =~ reg_exp_of_list [1; 2; 3].
Proof.
  simpl. apply (MApp [1]).
  { apply MChar. }
  apply (MApp [2]).
  { apply MChar. }
  apply (MApp [3]).
  { apply MChar. }
  apply MEmpty.
Qed.

Lemma MStar1 :
  forall T s (re : @reg_exp T) ,
    s =~ re ->
    s =~ Star re.
Proof.
  intros T s re H.
  rewrite <- (app_nil_r _ s).
  apply (MStarApp s [] re).
  - apply H.
  - apply MStar0.
Qed.

(*
Lemma empty_is_empty : ∀T (s : list T),
  ¬(s =~ EmptySet).
Proof.
  (* 请在此处解答 *) Admitted.
Lemma MUnion' : ∀T (s : list T) (re1 re2 : @reg_exp T),
  s =~ re1 ∨ s =~ re2 →
  s =~ Union re1 re2.
Proof.
  (* 请在此处解答 *) Admitted.
Lemma MStar' : ∀T (ss : list (list T)) (re : reg_exp),
  (∀s, In s ss → s =~ re) →
  fold app ss [] =~ Star re.
Proof.
  (* 请在此处解答 *) Admitted.
Lemma reg_exp_of_list_spec : ∀T (s1 s2 : list T),
  s1 =~ reg_exp_of_list s2 ↔ s1 = s2.
Proof.
  (* 请在此处解答 *) Admitted.

Fixpoint re_chars {T} (re : reg_exp) : list T :=
  match re with
  | EmptySet ⇒ []
  | EmptyStr ⇒ []
  | Char x ⇒ [x]
  | App re1 re2 ⇒ re_chars re1 ++ re_chars re2
  | Union re1 re2 ⇒ re_chars re1 ++ re_chars re2
  | Star re ⇒ re_chars re
  end.
Theorem in_re_match : ∀T (s : list T) (re : reg_exp) (x : T),
  s =~ re →
  In x s →
  In x (re_chars re).
Proof.
  intros T s re x Hmatch Hin.
  induction Hmatch
    as [| x'
        | s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2
        | s1 re1 re2 Hmatch IH | re1 s2 re2 Hmatch IH
        | re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2].
  (* 课上已完成 *)
  - (* MEmpty *)
    apply Hin.
  - (* MChar *)
    apply Hin.
  - simpl. rewrite In_app_iff in *.
    destruct Hin as [Hin | Hin].
    + (* In x s1 *)
      left. apply (IH1 Hin).
    + (* In x s2 *)
      right. apply (IH2 Hin).
  - (* MUnionL *)
    simpl. rewrite In_app_iff.
    left. apply (IH Hin).
  - (* MUnionR *)
    simpl. rewrite In_app_iff.
    right. apply (IH Hin).
  - (* MStar0 *)
    destruct Hin.
  - (* MStarApp *)
    simpl. rewrite In_app_iff in Hin.
    destruct Hin as [Hin | Hin].
    + (* In x s1 *)
      apply (IH1 Hin).
    + (* In x s2 *)
      apply (IH2 Hin).
Qed.

Fixpoint re_not_empty {T : Type} (re : @reg_exp T) : bool
  (* 将本行替换成 ":= _你的_定义_ ." *). Admitted.
Lemma re_not_empty_correct : ∀T (re : @reg_exp T),
  (∃s, s =~ re) ↔ re_not_empty re = true.
Proof.
  (* 请在此处解答 *) Admitted.

*)

Inductive reflect (P : Prop) : bool -> Prop :=
| ReflectT (H : P) : reflect P true
| ReflectF (H : ~P) : reflect P false.

Theorem iff_reflect : forall P b, (P <-> b = true) -> reflect P b.
Proof.
  (* 课上已完成 *)
  intros P b H. destruct b.
  - apply ReflectT. rewrite H. reflexivity.
  - apply ReflectF. rewrite H. intros H'. discriminate.
Qed.

Theorem reflect_iff : forall P b, reflect P b -> (P <-> b = true).
Proof.
  intros. destruct b.
  - inversion H. split. intros. reflexivity. intros. apply H0.
  - inversion H. split. intros.
    + apply H0 in H1. destruct H1.
    + intros. destruct H1. Admitted.

Lemma eqb_refl : forall n : nat,
  n =? n = true.
Proof.
  intros. induction n.
  - simpl. reflexivity.
  - simpl. apply IHn.
Qed.

Theorem eqb_eq : forall n1 n2 : nat,
  n1 =? n2 = true <-> n1 = n2.
Proof.
  intros n1 n2. split.
  - apply eqb_true.
  - intros H. rewrite H. rewrite <- eqb_refl with (n:=n2). reflexivity.
Qed.

Lemma eqbP : forall n m, reflect (n = m) (n =? m).
Proof.
  intros n m. apply iff_reflect. rewrite eqb_eq. reflexivity.
Qed.

Theorem filter_not_empty_In : forall n l,
  filter (fun x => n =? x) l <> [] ->
  In n l.
Proof.
  intros n l. induction l as [|m l' IHl'].
  - (* l =  *)
    simpl. intros H. apply H. reflexivity.
  - (* l = m :: l' *)
    simpl. destruct (n =? m) eqn:H.
    + (* n =? m = true *)
      intros _. rewrite eqb_eq in H. rewrite H.
      left. reflexivity.
    + (* n =? m = false *)
      intros H'. right. apply IHl'. apply H'.
Qed.

Theorem filter_not_empty_In' : forall n l,
  filter (fun x => n =? x) l <> [] ->
  In n l.
Proof.
  intros n l. induction l as [|m l' IHl'].
  - (* l =  *)
    simpl. intros H. apply H. reflexivity.
  - (* l = m :: l' *)
    simpl. destruct (eqbP n m) as [H | H].
    + (* n = m *)
      intros _. rewrite H. left. reflexivity.
    + (* n <> m *)
      intros H'. right. apply IHl'. apply H'.
Qed.

Fixpoint count n l :=
  match l with
  | [] => 0
  | m :: l' => (if n =? m then 1 else 0) + count n l'
  end.
Theorem eqbP_practice : forall n l,
  count n l = 0 -> ~(In n l).
Proof.
  Admitted.
Theorem not_all_tasks_finished : forall n:nat , True.
  Admitted.

repo: Coq


text:
Require Import Globalenvs Memory.
Require Import Csyntax Csem Cstrategy Coqlib Integers Values Maps Errors.
Require Import Arm6_State Arm6_Proc Arm6_SCC Bitvec Arm6.
Require Import mrs_compcert.
Require Import projection.
Require Import my_inversion.
Require Import my_tactic.
Require Import common_functions.

Require Import Arm6_Simul.
Import I.
Import Arm6_Functions.Semantics.

(* Add function CondictionPassed into global environment. *)
Definition fun_ConditionPassed :=
  common_functions.fun_ConditionPassed mrs_compcert.ConditionPassed.

Definition mrs_functions :=
  fun_ConditionPassed :: mrs_compcert.functions.

(* Re-new the program of MRS *)
Definition prog_mrs :=
  AST.mkprogram mrs_functions mrs_compcert.main mrs_compcert.global_variables.

Definition rbit_func_related (m:Mem.mem) (e:env) (rbit:bool):Prop:=
  bit_proj m e R = rbit.

Definition cond_func_related (m:Mem.mem) (e:env) (cond:opcode):Prop:=
  cond_proj mrs_compcert.cond m e = cond.

Definition d_func_related (m:Mem.mem) (e:env) (d:regnum):Prop:=
  reg_proj m e mrs_compcert.d = d.

Definition condpass :=
  Ecall (Evalof (Evar ConditionPassed T1) T1)
  (Econs
    (Eaddrof
      (Efield (Ederef (Evalof (Evar proc T2) T2) T3) cpsr T4)
      T5) (Econs (Evalof (Evar mrs_compcert.cond T6) T6) Enil)) T7.

(* A common proof on ConditionPass. It is nearly used in every instruction.
   Proofing its property in every instruction is a redundent work. It is
   neccessary to find a way to have a prove in common *)
(* Can't continue because of two reasons.
   First, ARM AST to CompcertC AST code generation doesn't consider the
   contents of function calls, if needed, we have to 'borrow' them from
   C to CompcertC code generation.
   Second, ConditionPass is an external function. No concrete value will be returned,
   only the type.
   The same as functions related to set_reg, them will call addr_of_reg, which
   is also a external function *)

Lemma no_effect_condpass :
  forall m0 e m0' m m' t v,
    alloc_variables empty_env m0
      (fun_internal_MRS.(fn_params) ++ fun_internal_MRS.(fn_vars)) e m0' ->
    eval_expression (Genv.globalenv prog_mrs) e m condpass t m' v ->
    m = m'.
Proof.
  intros until v;intros av ee.
  unfold condpass in ee.
  inv ee. rename H into ee, H0 into esrv.
  inv_eval_expr m m'.
  (* vres=v  *)
  inv esr0.
  (* vf is the value of ConditionPassed *)
  inv esr. rename H1 into esl,H4 into lvotvf. clear H2.
  (* e *)
  inv_alloc_vars av e.
  pose (e:=
    PTree.set d (b3, Tint I8 Unsigned)
      (PTree.set cond (b2, Tint I32 Signed)
        (PTree.set R (b0, Tint I8 Signed)
          (PTree.set proc (b1, Tpointer typ_SLv6_Processor)
            empty_env)))).
  fold e in eslst, esl.

  inv esl.
  (* ConditionPassed is not in local env *)
  discriminate.
  (* ConditionPassed is in global env *)
  rename H1 into notine,H2 into fs,H5 into tog.

  find_func.
  eapply mem_not_changed_ef in ev_funcall.
  exact ev_funcall.
Qed.

Lemma condpass_bool :
  forall m0 m0' e m t m' v cond s b,
    alloc_variables empty_env m0
    (fun_internal_MRS.(fn_params) ++ fun_internal_MRS.(fn_vars)) e m0' ->
    eval_expression (Genv.globalenv prog_mrs) e m condpass t m' v ->
    bool_val v T7 = Some b ->
    Arm6_Functions.State.ConditionPassed s cond = b.
Admitted.

Definition is_R_set :=
  Ebinop Oeq (Evalof (Evar R T7) T7)
  (Eval (Vint (repr 1)) T6) T6.

Lemma no_effect_is_R_set :
  forall e m t m' v,
    eval_expression (Genv.globalenv prog_mrs) e m is_R_set t m' v ->
    m = m'.
Proof.
  intros until v; intro ee_binop.
  inv ee_binop. rename H into ee_binop, H0 into esrv.
  unfold is_R_set in ee_binop.
  inv_binop m m'. intros until a2'. intros ee_valof ee_val esrv.
  inv_valof m m'0. intros until a'0. intros ee_var esrv.
  inv_var m m'0.
  inv_val m m'. intro esrv.
  reflexivity.
Qed.

Lemma R_bool :
  forall m0 e m0' m t m' v rbit b,
    alloc_variables empty_env m0
      (fun_internal_MRS.(fn_params) ++ fun_internal_MRS.(fn_vars)) e m0' ->
    rbit_func_related m e rbit->
    eval_expression (Genv.globalenv prog_mrs) e m is_R_set t m' v ->
    bool_val v T7 = Some b->
    Util.zeq rbit 1 = b.
Proof.
  intros until b. intros av rfrel ee_R bvv.
  unfold rbit_func_related in rfrel. unfold bit_proj in rfrel.
  unfold param_val in rfrel.
  inv_alloc_vars av e.
  pose (e:=
    PTree.set d (b3, Tint I8 Unsigned)
      (PTree.set cond (b2, Tint I32 Signed)
        (PTree.set R (b0, Tint I8 Signed)
          (PTree.set proc (b1, Tpointer typ_SLv6_Processor)
            empty_env)))).
  fold e in ee_R |-*;simpl.
  inv ee_R. rename H into ee_R, H0 into esrv.
  unfold is_R_set in ee_R.
  inv_binop m m'. intros until a2'. intros ee_valof ee_val esrv.
  inv_valof m m'0. intros until a'0. intros ee_var esrv.
  inv_var m m'0.
  inv_val m m'. intros esrv.
  inv esrv. rename H4 into esrv1, H5 into esrv2, H6 into sbo.
  inv esrv2.
  inv esrv1. rename H1 into esl, H4 into lvotv1. clear H2.
  simpl in sbo.
  inv esl;try discriminate. rename H3 into existR.
  simpl in existR;injection existR;clear existR;intros eq04;rewrite<-eq04 in *;
    clear b4 eq04.
  unfold T7 in lvotv1.
  rewrite lvotv1.
  unfold sem_cmp in sbo;simpl in sbo.
  destruct v1; try discriminate.
  injection sbo. clear sbo;intro eqv;rewrite<-eqv in *;clear eqv v.
  unfold varg_proj.
  unfold bool_val in bvv;simpl in bvv. unfold w1.
  unfold Val.of_bool in bvv;simpl in bvv.
  destruct (eq i (repr 1));simpl in bvv;injection bvv;intro eq;rewrite<-eq;simpl;
    reflexivity.
Qed.

Definition set_reg_pc_spsr :=
  Ecall (Evalof (Evar set_reg_or_pc T8) T8)
  (Econs (Evalof (Evar proc T2) T2)
    (Econs (Evalof (Evar mrs_compcert.d T9) T9)
      (Econs
        (Ecall
          (Evalof (Evar StatusRegister_to_uint32 T10) T10)
          (Econs
            (Ecall (Evalof (Evar spsr T11) T11)
              (Econs (Evalof (Evar proc T2) T2) Enil) T5)
            Enil) T12) Enil))) T13.

Definition set_reg_pc_cpsr :=
  Ecall (Evalof (Evar set_reg_or_pc T8) T8)
  (Econs (Evalof (Evar proc T2) T2)
    (Econs (Evalof (Evar mrs_compcert.d T9) T9)
      (Econs
        (Ecall
          (Evalof (Evar StatusRegister_to_uint32 T10) T10)
          (Econs
            (Eaddrof
              (Efield
                (Ederef (Evalof (Evar proc T2) T2) T3)
                cpsr T4) T4) Enil) T12) Enil))) T13.

Lemma setregpc_spsr_ok :
  forall m e l b s t m' v d,
    proc_state_related proc m e (Ok tt (mk_semstate l b s))->
    eval_expression (Genv.globalenv prog_mrs) e m set_reg_pc_spsr t m' v ->
    proc_state_related proc m' e
    (match Arm6_State.mode s with
       | usr =>
         unpredictable Arm6_Message.EmptyMessage
         {| loc := nil; bo := true; st := s |}
       | exn em =>
         set_reg d (Arm6_State.spsr s em)
         {| loc := nil; bo := true; st := s |}
       | sys =>
         unpredictable Arm6_Message.EmptyMessage
         {| loc := nil; bo := true; st := s |}
     end).
Admitted.

Lemma setregpc_cpsr_ok :
  forall m e l b s t m' v b' d,
    proc_state_related proc m e (Ok tt (mk_semstate l b s))->
    eval_expression (Genv.globalenv prog_mrs) e m set_reg_pc_cpsr t m' v ->
    proc_state_related proc m' e
    (Ok tt (mk_semstate l b'
      (Arm6_State.set_reg s d (Arm6_State.cpsr s)))).
Admitted.

(*
Lemma R_not_change_setregpc :
  forall e m t m' a' R,
    rbit_func_related m e R ->
    eval_expr (Genv.globalenv prog_mrs) e m RV set_reg_pc_spsr t m' a'->
    rbit_func_related m' e R.
Admitted.

Lemma cond_not_change_setregpc :
  forall e m t m' a' cd,
    cond_func_related m e cd ->
    eval_expr (Genv.globalenv prog_mrs) e m RV set_reg_pc_spsr t m' a'->
    cond_func_related m' e cd.
Admitted.

Lemma d_not_changed_setregpc :
  forall e m t m' a' d,
    d_func_related m e d ->
    eval_expr (Genv.globalenv prog_mrs) e m RV set_reg_pc_spsr t m' a'->
    d_func_related m' e d.
Admitted.
*)

Theorem correctness_MSR : forall e m0 m1 m2 mfin vargs s out rbit cond d,
  alloc_variables empty_env m0
  (fun_internal_MRS.(fn_params)++fun_internal_MRS.(fn_vars)) e m1->
  bind_parameters e m1 fun_internal_MRS.(fn_params) vargs m2->
  proc_state_related proc m2 e (Ok tt (mk_semstate nil true s)) ->
  rbit_func_related m2 e rbit ->
  cond_func_related m2 e cond ->
  d_func_related m2 e d ->
  exec_stmt (Genv.globalenv prog_mrs) e m2 fun_internal_MRS.(fn_body)
  Events.E0 mfin out ->
  proc_state_related proc mfin e
  (S.MRS_step rbit cond d (mk_semstate nil true s)).
Proof.
  intros until d;intros av bp psrel rfrel cfrel dfrel exst.

  (* unfold MRS in C side *)
  inv exst. rename H5 into ee_cp, H8 into bvv1, H9 into exst, H4 into events.
  simpl in bvv1.
  generalize ee_cp; intro ee_cp'.

  (* m2 = m3 *)
  apply no_effect_condpass with m0 e m1 m2 m3 t1 v1 in ee_cp';[idtac| assumption].
  rewrite<-ee_cp' in *;clear m3 ee_cp'.

  (* condition pass gives the same result in two side *)
  generalize av; intro av'.
  apply condpass_bool with m0 m1 e m2 t1 m2 v1 cond s b in av';
    [idtac|exact ee_cp|exact bvv1].
  clear ee_cp.

  (* case on the boolean value of condpass *)
  destruct b.

    (* condpass = true *)
    inv exst. rename H4 into ee_binop, H8 into bvv0, H9 into exst.
    simpl in bvv0.

    (* m2 = m3 *)
    generalize ee_binop;intro ee_binop'.
    apply no_effect_is_R_set with e m2 t0 m3 v0 in ee_binop'.
    rewrite<-ee_binop' in *;clear m3 ee_binop'.

    (* R has the same value in two sides *)
    apply R_bool with m0 e m1 m2 t0 m2 v0 rbit b in av;
      [idtac|exact rfrel|exact ee_binop|exact bvv0].

    (* case on R bit *)
    destruct b.

      (* R = 1 *)
      inv exst. rename H2 into ee_call.
      apply setregpc_spsr_ok with m2 e nil true s t3 mfin v d in psrel;
        [idtac|exact ee_call].

      (* unfold MRS in Coq side *)
      unfold S.MRS_step. unfold _get_st. unfold bind_s.
      unfold bind; simpl.
      rewrite av'; simpl.
      rewrite av; simpl.

      unfold if_CurrentModeHasSPSR;simpl.
      exact psrel.

      (* R = 0 *)
      inv exst. rename H2 into ee_call.
      apply setregpc_cpsr_ok with m2 e nil true s t3 mfin v (Util.zne d 15) d
        in psrel; [idtac|exact ee_call].

      (* unfold MRS in Coq side *)
      unfold S.MRS_step. unfold _get_st. unfold bind_s.
      unfold bind;simpl.
      rewrite av';simpl.
      rewrite av;simpl.
      unfold set_reg. simpl. unfold _Arm_State.set_reg.
      exact psrel.

    (* if condition pass is false *)
    inv exst.

    (* unfold MRS in Coq side *)
    unfold S.MRS_step. unfold _get_st. unfold bind_s.
    unfold bind;simpl.
    rewrite av';simpl.
    exact psrel.
Qed.

author: git-inria

repo: simsoc-cert

save_path: github-repos/coq/git-inria-simsoc-cert


text:
Definition tic_tac_toe_game : relaxed.game.
refine {|
   relaxed.possible_move := nat * nat
 ; relaxed.first_player := player_P
 ; relaxed.next_player moves_so_far := if Nat.even (List.length moves_so_far)
                                       then player_P else player_O
 ; relaxed.play_won_by_P all_moves
   := exists n : nat,
     tic_tac_toe.game_outcome
       (Streams.firstn all_moves n) tic_tac_toe.initial_state
     == Some tic_tac_toe.player_1
 ; relaxed.play_won_by_O all_moves
   := exists n : nat,
     tic_tac_toe.game_outcome
       (Streams.firstn all_moves n) tic_tac_toe.initial_state
     == Some tic_tac_toe.player_2
 ; relaxed.next_move_is_valid := tic_tac_toe.next_move_is_valid_or_game_finished
  |}.

author: harshikaaagrawal

repo: game-semantics-for-affine-logic


text:
(** DWFM soundness proofs - The core calculus. *)
From stdpp Require Import strings gmap.
From mathcomp Require Import ssreflect.

(** The core language. Difference to ESOP submission: recursive functions added. *)
Definition loc := positive.
Definition tid := positive.
Variant const := Ctrue | Cfalse | Cunit | Cloc (l: loc) | Ctid (t: tid).
Variant binder := BAnon | BNamed (x: string).
Inductive expr :=
| Const (c: const)
| Var (x: string)
| Rec (f x: binder) (e: expr)
| App (e e': expr)
| If (e e' e'': expr)
| Alloc (e: expr)
| Read (e: expr)
| Write (e e': expr)
| Post (e: expr)
| Wait (e: expr).
Coercion Const: const >-> expr.
Coercion Var: string >-> expr.
Definition singleton' b: gset string := match b with BNamed x => {[x]} | BAnon => ∅ end.
Notation "{[? b ]}" := (singleton' b).
Inductive Closed: gset string → expr → Prop :=
| const_closed X c: Closed X (Const c)
| var_closed X x: x ∈ X → Closed X (Var x)
| rec_closed X f x e: Closed ({[? f]} ∪ {[? x ]} ∪ X) e → Closed X (Rec f x e)
| app_closed X e₁ e₂: Closed X e₁ → Closed X e₂ → Closed X (App e₁ e₂)
| if_closed X e₁ e₂ e₃: Closed X e₁ → Closed X e₂ → Closed X e₃ → Closed X (If e₁ e₂ e₃)
| alloc_closed X e₁: Closed X e₁ → Closed X (Alloc e₁)
| read_closed X e₁: Closed X e₁ → Closed X (Read e₁)
| write_closed X e₁ e₂: Closed X e₁ → Closed X e₂ → Closed X (Write e₁ e₂)
| post_closed X e₁: Closed X e₁ → Closed X (Post e₁)
| wait_closed X e₁: Closed X e₁ → Closed X (Wait e₁).
Instance expr_eq_dec: EqDecision expr.
Proof. cbv -[not]. repeat decide equality. Qed.

Instance: ∀ X e, ProofIrrel (Closed X e).
Proof.
  enough (∀ X X' e e' (eqX: X = X') (eqe: e = e') (H: Closed X e) (H': Closed X' e'),
             H = eq_rect_r (Closed X) (eq_rect_r (λ X, Closed X e') H' eqX) eqe)
    as irr.
  { intros; red; apply (irr X X e e eq_refl eq_refl). }
  fix IH 7.
  intros.
  destruct H, H'; try discriminate.
  all: subst; injection eqe; subst; repeat intros <-.
  all: try (pattern eqe; apply (Eqdep_dec.K_dec_type expr_eq_dec); cbn; f_equal).
  all: try apply (IH _ _ _ _ eq_refl eq_refl).
  Guarded.
  apply eq_pi, _.
Qed.
Instance: ∀ X e, Decision (Closed X e).
Proof.
  fix IH 2.
  destruct e; cbn.
  6,7,9,10: destruct (IH X e); last by right; inversion_clear 1.
  4,5,10: destruct (IH X e1); last by right; inversion_clear 1.
  4,5,6: destruct (IH X e2); last by right; inversion_clear 1.
  5: destruct (IH X e3); last by right; inversion_clear 1.
  2: destruct (decide (x ∈ X)); last by right; inversion_clear 1.
  3: destruct (IH ({[? f]} ∪ {[? x ]} ∪ X) e); last by right; inversion_clear 1.
  all: by left; constructor.
Defined.

Variant val :=
| VConst (c: const)
| VRec (f x: binder) (e: expr) {e_closed: Closed ({[? f]} ∪ {[? x ]}) e}.
Coercion VConst: const >-> val.

Variant ctx_item :=
| CAppL (e': expr)
| CAppR (v: val)
| CIf (e' e'': expr)
| CAlloc
| CRead
| CWriteL (e': expr)
| CWriteR (v: val)
| CWait.
Variant ectx_item :=
| ERec (f x: binder)
| EAppL (e': expr)
| EAppR (e: expr)
| EIfL (e' e'': expr)
| EIfM (e e'': expr)
| EIfR (e e': expr)
| EAlloc
| ERead
| EWriteL (e': expr)
| EWriteR (e: expr)
| EPost
| EWait.

Definition of_val v :=
  match v with
  | VConst c => Const c
  | VRec f x e _ => Rec f x e
  end.
Definition to_val e :=
  match e with
  | Const c => Some (VConst c)
  | Rec f x e => match decide (Closed ({[? f]} ∪ {[? x]}) e) with
                 | left H => Some (@VRec f x e H)
                 | right _ => None
                 end
  | _ => None
  end.

Definition fill_ctx_item e c :=
  match c with
  | CAppL e' => App e e'
  | CAppR v => App (of_val v) e
  | CIf e' e'' => If e e' e''
  | CAlloc => Alloc e
  | CRead => Read e
  | CWriteL e' => Write e e'
  | CWriteR v => Write (of_val v) e
  | CWait => Wait e
  end.
Definition fill_ectx_item e c :=
  match c with
  | ERec f x => Rec f x e
  | EAppL e' => App e e'
  | EAppR e' => App e' e
  | EIfL e' e'' => If e e' e''
  | EIfM e' e'' => If e' e e''
  | EIfR e' e'' => If e' e'' e
  | EAlloc => Alloc e
  | ERead => Read e
  | EWriteL e' => Write e e'
  | EWriteR e' => Write e' e
  | EPost => Post e
  | EWait => Wait e
  end.
Definition fill_ctx := foldl fill_ctx_item.
Definition fill_ectx := foldl fill_ectx_item.

Definition delete' {A} b (m: gmap string A) :=
  match b with BAnon => m | BNamed x => delete x m end.

Fixpoint subst σ e :=
  let s := subst σ in
  match e with
  | Const l => Const l
  | Var x => match σ !! x with Some e => e | None => Var x end
  | Rec f x e => Rec f x (subst (delete' f (delete' x σ)) e)
  | App e e' => App (s e) (s e')
  | Alloc e => Alloc (s e)
  | Read e => Read (s e)
  | Write e e' => Write (s e) (s e')
  | If e e' e'' => If (s e) (s e') (s e'')
  | Post e => Post (s e)
  | Wait e => Wait (s e)
  end.
Definition subst' b e e' :=
  match b with BAnon => e' | BNamed x => subst (<[x:=e]>∅) e' end.

Definition subst_ctx_item σ i :=
  match i with
  | CAppL e' => CAppL (subst σ e')
  | CAppR v => CAppR v
  | CIf e' e'' => CIf (subst σ e') (subst σ e'')
  | CAlloc => CAlloc
  | CRead => CRead
  | CWriteL e' => CWriteL (subst σ e')
  | CWriteR v => CWriteR v
  | CWait => CWait
  end.
Definition subst_ctx σ (K: list ctx_item) := subst_ctx_item σ <$> K.

Local Opaque union.
Lemma elem_of_singleton' b x: x ∈ {[? b ]} ↔ BNamed x = b.
Proof.
  destruct b; rewrite /= ?elem_of_singleton ?elem_of_empty;
    intuition congruence.
Qed.
Lemma lookup_delete' {A} b (v: A) m x: delete' b m !! x = Some v ↔ BNamed x ≠ b ∧ m !! x = Some v.
Proof with try intuition congruence.
  destruct b as [|y]; rewrite /=...
  destruct (decide (x=y)) as [<-|neq].
  - rewrite lookup_delete...
  - rewrite lookup_delete_ne...
Qed.
Lemma lookup_delete'_None {A} b (m: gmap string A) x:
  delete' b m !! x = None ↔ BNamed x = b ∨ m!!x = None.
Proof.
  destruct b as [|y]; cbn.
  - intuition discriminate.
  - destruct (decide (x=y)) as [<-|neq].
    + rewrite lookup_delete; tauto.
    + rewrite lookup_delete_ne; intuition congruence.
Qed.

Instance: EqDecision binder.
Proof. solve_decision. Qed.

Lemma lookup_delete'_cases {A} b x (m: gmap string A):
  delete' b m !! x = if bool_decide (BNamed x ≠ b) then m!!x else None.
Proof.
  destruct (bool_decide_reflect (BNamed x ≠ b)) as [case|case].
  - apply option_eq; intro v.
    rewrite lookup_delete'; tauto.
  - apply lookup_delete'_None.
    left; by apply dec_stable.
Qed.

Lemma subst_closed X e: Closed X e → ∀ σ (disj: ∀ x, x ∈ X → σ !! x = None), subst σ e = e.
Proof.
  induction 1; intros.
  all: rewrite /= ?IHClosed ?IHClosed1 ?IHClosed2 ?IHClosed3; auto.
  - rewrite disj //.
  - intros y.
    rewrite !elem_of_union !elem_of_singleton' !lookup_delete'_None.
    intuition.
Qed.

Lemma subst_closed_empty e σ: Closed ∅ e → subst σ e = e.
Proof.
  intro; apply (subst_closed ∅); auto.
  set_solver.
Qed.

Instance Closed_proper: Proper ((≡) ==> eq ==> iff) Closed.
Proof. by intros ?? <-%leibniz_equiv ?? <-. Qed.

Lemma val_closed v: Closed ∅ (of_val v).
Proof.
  destruct v; constructor.
  rewrite right_id; done.
Qed.

Corollary subst_val v σ: subst σ (of_val v) = of_val v.
Proof. apply subst_closed_empty, val_closed. Qed.

Lemma subst_fill σ K e: subst σ (fill_ctx e K) = fill_ctx (subst σ e) (subst_ctx σ K).
Proof.
  revert e; unfold subst_ctx.
  induction K as [|I K IH]; cbn; intros; first done.
  rewrite IH; f_equal.
  destruct I; try done.
  all: rewrite /= subst_val //.
Qed.

Hint Constructors Closed.
Lemma closed_mono: Proper ((⊆) ==> (=) ==> impl) Closed.
Proof.
  intros X X' sub e ? <- closed; revert X' sub.
  induction closed; eauto.
  intros; constructor.
  apply IHclosed.
  clear -sub; set_solver.
Qed.

Lemma closed_subst X e: Closed X e → ∀ σ (closed: ∀ x e, x ∈ X → σ !! x = Some e →
                                                         Closed X e),
      Closed X (subst σ e).
Proof.
  induction 1; cbn; eauto; intros.
  - destruct (σ!!x) as [e|] eqn:mt.
    + by apply (closed x).
    + by constructor.
  - constructor.
    apply IHClosed.
    intros x' e'.
    rewrite !elem_of_union !elem_of_singleton' !lookup_delete'.
    intros [[?|?]|inx'].
    1,2: tauto.
    intros [_ [_ mt]].
    generalize (closed x' e' inx' mt).
    apply closed_mono; auto.
    clear; set_solver.
Qed.

Lemma closed_subst_val X e σ: Closed X e → Closed X (subst (of_val <$> σ) e).
Proof.
  intro closed.
  apply closed_subst; auto.
  intros x e' inx.
  rewrite lookup_fmap fmap_Some.
  intros [v [_ ->]].
  eapply closed_mono.
  - apply empty_subseteq.
  - done.
  - apply val_closed.
Qed.

Definition subst_merge' σ e e' :=
  match e' with
  | Some e' => Some (subst σ e')
  | None => e
  end.
Instance: ∀ σ, DiagNone (subst_merge' σ).
Proof. done. Qed.

Definition subst_merge σ σ' := merge (subst_merge' σ) σ σ'.

Lemma subst_subst σ σ' e:
  (∀ x e, σ' !! x = Some e → Closed ∅ e) →
  subst σ (subst σ' e) = subst (subst_merge σ σ') e.
Proof.
  revert σ σ'.
  induction e; intros ?? good_subst; cbn.
  all: rewrite ?IHe ?IHe1 ?IHe2 ?IHe3; auto.
  { rewrite /subst_merge lookup_merge.
    destruct (σ' !! x) as [e'|] eqn:subst'; done. }
  { apply f_equal, (f_equal (λ σ, subst σ e)), map_eq; intro y.
    apply option_eq; intro e'.
    rewrite /subst_merge lookup_merge /subst_merge' !lookup_delete' lookup_merge
            lookup_delete'_cases.
    destruct (bool_decide_reflect (BNamed y ≠ f)) as [neqy|<-%dec_stable]; cycle 1.
    { rewrite lookup_delete; intuition congruence. }
    rewrite lookup_delete'_cases.
    destruct (bool_decide_reflect (BNamed y ≠ x)) as [neqx|<-%dec_stable]; cycle 1.
    { rewrite lookup_delete' lookup_delete; intuition congruence. }
    destruct (σ' !! y) as [e''|] eqn:mty.
    + rewrite !subst_closed_empty; eauto; tauto.
    + by rewrite !lookup_delete'. }
  { intros x' e'.
    rewrite !lookup_delete'; intuition eauto. }
Qed.

Lemma subst_insert_r σ x e e' (e_closed: Closed ∅ e):
  subst (<[x:=e]>σ) e' =
  subst σ (subst (<[x:=e]>∅) e').
Proof.
  rewrite subst_subst.
  { apply (f_equal (λ σ, subst σ e')), map_eq; intro y.
    rewrite /subst_merge lookup_merge.
    destruct (decide (x=y)) as [<-|neq].
    - by rewrite !lookup_insert /= subst_closed_empty.
    - by rewrite !lookup_insert_ne ?lookup_empty /=. }
  intros x' e''.
  rewrite lookup_insert_Some lookup_empty.
  intuition congruence.
Qed.

Lemma fill_ctx_app K K' e: fill_ctx (fill_ctx e K) K' = fill_ctx e (K++K').
Proof. by rewrite /fill_ctx foldl_app. Qed.
Lemma fill_ectx_app K K' e: fill_ectx (fill_ectx e K) K' = fill_ectx e (K++K').
Proof. by rewrite /fill_ectx foldl_app. Qed.

Definition heap := gmap loc val.
Variant task_state := running (e: expr) | done (v: val).
Definition task_buffer := gmap tid task_state.

Variant head_step (p: tid): expr → heap → task_buffer → expr → heap → task_buffer → Prop :=
| step_app f x e e' v h t:
    to_val e' = Some v →
    head_step p (App (Rec f x e) e') h t (subst' f (Rec f x e) (subst' x e' e)) h t
| step_if_true e' e'' h t:
    head_step p (If (Const Ctrue) e' e'') h t e' h t
| step_if_false e' e'' h t:
    head_step p (If (Const Cfalse) e' e'') h t e'' h t
| step_alloc e v h t l:
    to_val e = Some v →
    h !! l = None →
    head_step p (Alloc e) h t (Cloc l) (<[l:=v]>h) t
| step_read l h t v:
    h !! l = Some v →
    head_step p (Read (Cloc l)) h t (of_val v) h t
| step_write l e' v h t:
    to_val e' = Some v →
    is_Some (h!!l) →
    head_step p (Write (Cloc l) e') h t Cunit (<[l:=v]>h) t
| step_post e p' h t:
    t !! p' = None →
    p ≠ p' →
    head_step p (Post e) h t (Ctid p') h (<[p':=running e]>t)
| step_wait_done p' h t v:
    t !! p' = Some (done v) →
    head_step p (Wait (Ctid p')) h t (of_val v) h t.
Variant local_step (p: tid): expr → heap → task_buffer → expr → heap → task_buffer → Prop :=
| local_step_from_head_step K e h t e' h' t':
    head_step p e h t e' h' t' →
    local_step p (fill_ctx e K) h t (fill_ctx e' K) h' t'.

Definition is_running (t: task_buffer) p := ∃ e, t !! p = Some (running e).

Variant global_step: heap → task_buffer → tid → heap → task_buffer → tid → Prop :=
| global_local p h t h' t' e e':
    t !! p = Some (running e) → t' !! p = Some (running e') →
    local_step p e h (delete p t) e' h' (delete p t') →
    global_step h t p h' t' p
| global_wait_schedule h t K p p' p'':
    t !! p = Some (running (fill_ctx (Wait (Ctid p'')) K)) →
    is_running t p' →
    global_step h t p h t p'
| global_done_schedule h t p p' v e:
    to_val e = Some v →
    t !! p = Some (running e) →
    is_running t p' →
    global_step h t p h (<[p := done v]>t) p'.

Definition reducible e := ∃ p T H e' T' H', head_step p e T H e' T' H'.
Definition stuck e := ¬reducible e.
Definition atomic e := reducible e ∧ ∀ p T H e' T' H', head_step p e T H e' T' H' → stuck e'.

Lemma to_of_val v: to_val (of_val v) = Some v.
Proof.
  destruct v; first done.
  rewrite /= decide_left; done.
Qed.

Lemma of_to_val e v: to_val e = Some v → of_val v = e.
Proof.
  destruct e; try done.
  - destruct v; last done.
    injection 1 as <-; done.
  - cbn.
    destruct decide; simplify_eq 1.
    intros <-; done.
Qed.

author: johanneskloos

repo: esop

save_path: github-repos/coq/johanneskloos-esop


text:
(* Copyright © 1998-2006
 * Henk Barendregt
 * Luís Cruz-Filipe
 * Herman Geuvers
 * Mariusz Giero
 * Rik van Ginneken
 * Dimitri Hendriks
 * Sébastien Hinderer
 * Bart Kirkels
 * Pierre Letouzey
 * Iris Loeb
 * Lionel Mamane
 * Milad Niqui
 * Russell O’Connor
 * Randy Pollack
 * Nickolay V. Shmyrev
 * Bas Spitters
 * Dan Synek
 * Freek Wiedijk
 * Jan Zwanenburg
 *
 * This work is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * This work is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License along
 * with this work; if not, write to the Free Software Foundation, Inc.,
 * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
 *)

Require Export CoRN.complex.CComplex.
Import CRing_Homomorphisms.coercions.
From Coq Require Import Lia.

(**
* Shifting polynomials
This can be done for [CRings] in general, but we do it here
only for [CC] because extensionality makes everything much easier,
and we only need it for [CC].
*)

Section Poly_Shifted.

Definition Shift (a : CC) (p : CCX) :=
  Sum 0 (lth_of_poly p) (fun i => _C_ (nth_coeff i p) [*] (_X_[+]_C_ a) [^]i).

Lemma Shift_apply : forall a p (x : CC), (Shift a p) ! x [=] p ! (x[+]a).
Proof.
 intros.
 unfold Shift in |- *.
 apply eq_transitive_unfolded with (Sum 0 (lth_of_poly p)
   (fun i : nat => (_C_ (nth_coeff i p) [*] (_X_[+]_C_ a) [^]i) ! x)).
  apply Sum_cpoly_ap with (f := fun i : nat => _C_ (nth_coeff i p) [*] (_X_[+]_C_ a) [^]i).
 apply eq_symmetric_unfolded.
 astepl (Sum 0 (lth_of_poly p) (fun i : nat => _C_ (nth_coeff i p) [*]_X_[^]i)) ! (x[+]a).
 apply eq_transitive_unfolded with (Sum 0 (lth_of_poly p)
   (fun i : nat => (_C_ (nth_coeff i p) [*]_X_[^]i) ! (x[+]a))).
  apply Sum_cpoly_ap with (f := fun i : nat => _C_ (nth_coeff i p) [*]_X_[^]i).
 apply Sum_wd. intros.
 astepl ((_C_ (nth_coeff i p)) ! (x[+]a) [*] (_X_[^]i) ! (x[+]a)).
 astepl (nth_coeff i p[*]_X_ ! (x[+]a) [^]i).
 astepl (nth_coeff i p[*] (x[+]a) [^]i).
 astepl (nth_coeff i p[*] (_X_ ! x[+] (_C_ a) ! x) [^]i).
 astepl (nth_coeff i p[*] (_X_[+]_C_ a) ! x[^]i).
 Step_final ((_C_ (nth_coeff i p)) ! x[*] ((_X_[+]_C_ a) [^]i) ! x).
Qed.

Hint Resolve Shift_apply: algebra.

Lemma Shift_wdr : forall a p p', p [=] p' -> Shift a p [=] Shift a p'.
Proof.
 intros. apply poly_CC_extensional. intros.
 astepl p ! (x[+]a). Step_final p' ! (x[+]a).
Qed.

Lemma Shift_shift : forall a p, Shift [--]a (Shift a p) [=] p.
Proof.
 intros. apply poly_CC_extensional. intros.
 astepl (Shift a p) ! (x[+][--]a).
 astepl p ! (x[+][--]a[+]a).
 apply apply_wd. algebra. rational.
Qed.

Lemma Shift_mult : forall a p1 p2, Shift a (p1[*]p2) [=] Shift a p1[*]Shift a p2.
Proof.
 intros. apply poly_CC_extensional. intros.
 astepl (p1[*]p2) ! (x[+]a).
 astepl (p1 ! (x[+]a) [*]p2 ! (x[+]a)).
 Step_final ((Shift a p1) ! x[*] (Shift a p2) ! x).
Qed.

Lemma Shift_degree_le : forall a p n, degree_le n p -> degree_le n (Shift a p).
Proof.
 intros.
 unfold Shift in |- *.
 apply Sum_degree_le. auto with arith. intros.
  elim (le_lt_dec i n); intros.
  replace n with (0 + n).
   apply degree_le_mult. apply degree_le_c_.
    apply degree_le_mon with (1 * i).
    lia.
   apply degree_le_nexp. apply degree_imp_degree_le.
   apply degree_wd with (_C_ a[+]_X_). algebra.
    apply degree_plus_rht with 0. apply degree_le_c_. apply degree_x_.
     auto. auto.
  unfold degree_le in H.
 apply degree_le_wd with (_C_ ([0]:CC)).
  astepl ([0]:cpoly_cring CC).
  astepl ([0][*] (_X_[+]_C_ a) [^]i).
  apply bin_op_wd_unfolded.
   Step_final (_C_ ([0]:CC)).
  algebra.
 apply degree_le_mon with 0.
  auto with arith.
 apply degree_le_c_.
Qed.

Lemma Shift_monic : forall a p n, monic n p -> monic n (Shift a p).
Proof.
 intros.
 unfold monic in H. elim H. clear H. intros H H0. unfold degree_le in H0.
 apply monic_wd with (Sum 0 n (fun i : nat => _C_ (nth_coeff i p) [*] (_X_[+]_C_ a) [^]i)).
  astepl (Sum 0 n (fun i : nat => _C_ (nth_coeff i p) [*] (_X_[+]_C_ a) [^]i) [+][0]).
  apply eq_transitive_unfolded with
    (Sum 0 n (fun i : nat => _C_ (nth_coeff i p) [*] (_X_[+]_C_ a) [^]i) [+] Sum (S n) (lth_of_poly p)
      (fun i : nat => _C_ (nth_coeff i p) [*] (_X_[+]_C_ a) [^]i)).
   apply bin_op_wd_unfolded. algebra.
    apply eq_symmetric_unfolded.
   apply Sum_zero.
    cut (n < lth_of_poly p). intro. auto with arith.
     apply lt_i_lth_of_poly. astepl ([1]:CC). algebra.
    intros. cut (n < i). intro.
   astepl (_C_ [0][*] (_X_[+]_C_ a) [^]i).
    Step_final ([0][*] (_X_[+]_C_ a) [^]i).
   auto with arith.
  unfold Shift in |- *.
  apply Sum_Sum.
 elim (O_or_S n); intro y. elim y. clear y. intros x y.
  rewrite <- y in H. rewrite <- y in H0. rewrite <- y.
  apply monic_wd with (Sum 0 x (fun i : nat => _C_ (nth_coeff i p) [*] (_X_[+]_C_ a) [^]i) [+]
    (_X_[+]_C_ a) [^]S x).
   apply eq_transitive_unfolded with
     (Sum 0 x (fun i : nat => _C_ (nth_coeff i p) [*] (_X_[+]_C_ a) [^]i) [+]
       _C_ (nth_coeff (S x) p) [*] (_X_[+]_C_ a) [^]S x).
    apply bin_op_wd_unfolded. algebra.
     astepl ([1][*] (_X_[+]_C_ a) [^]S x).
    apply bin_op_wd_unfolded.
     Step_final (_C_ ([1]:CC)). algebra.
    apply eq_symmetric_unfolded.
   apply Sum_last with (f := fun i : nat => _C_ (nth_coeff i p) [*] (_X_[+]_C_ a) [^]i).
  apply monic_plus with x.
    apply Sum_degree_le. auto with arith. intros.
     replace x with (0 + x).
     apply degree_le_mult. apply degree_le_c_.
      apply degree_le_mon with (1 * i).
      lia.
     apply degree_le_nexp. apply degree_imp_degree_le.
     apply degree_wd with (_C_ a[+]_X_). algebra.
      apply degree_plus_rht with 0. apply degree_le_c_. apply degree_x_.
       auto. auto.
    pattern (S x) at 1 in |- *. replace (S x) with (1 * S x).
   apply monic_nexp.
    apply monic_wd with (_C_ a[+]_X_). algebra.
     apply monic_plus with 0. apply degree_le_c_.
      apply monic_x_.
    auto. auto with arith. auto.
   rewrite <- y in H. rewrite <- y in H0. rewrite <- y.
 apply monic_wd with ([1]:CCX).
  unfold Sum in |- *. unfold Sum1 in |- *. simpl in |- *. split.
  cut ([1] [=] nth_coeff 0 p[*][1][+][0]). auto.
    astepl (nth_coeff 0 p). rational. auto.
   apply monic_wd with (_C_ ([1]:CC)). algebra.
  apply monic_c_one.
Qed.

End Poly_Shifted.

#[global]
Hint Resolve Shift_wdr: algebra_c.
#[global]
Hint Resolve Shift_apply Shift_shift Shift_mult: algebra.

author: coq-community

repo: corn

save_path: github-repos/coq/coq-community-corn