text:
Require Import rt.util.all.
Require Import rt.model.priority.
Require Import rt.model.arrival.basic.task.
Require Import rt.model.schedule.uni.schedulability.
Require Import rt.model.arrival.jitter.job.
Require Import rt.model.schedule.uni.jitter.schedule.
Require Import rt.analysis.uni.jitter.workload_bound_fp
               rt.analysis.uni.jitter.fp_rta_comp.
Require Import rt.implementation.uni.jitter.job
               rt.implementation.uni.jitter.task
               rt.implementation.uni.jitter.arrival_sequence
               rt.implementation.uni.jitter.schedule.
From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.

Module ResponseTimeAnalysisFP.

  Import JobWithJitter UniprocessorScheduleWithJitter SporadicTaskset Priority Schedulability
         WorkloadBoundFP ResponseTimeIterationFP.
  Import ConcreteJob ConcreteTask ConcreteArrivalSequence ConcreteScheduler.

  (* In this section, we test the jitter-aware FP RTA on a simple task set
     to show that the theorems contain no contradictory assumptions. *)
  Section ExampleRTA.

    Let tsk1 := {| task_id := 1; task_cost := 1; task_period := 5;
                                 task_deadline := 6; task_jitter := 1 |}.
    Let tsk2 := {| task_id := 2; task_cost := 1; task_period := 5;
                                 task_deadline := 6; task_jitter := 0|}.
    Let tsk3 := {| task_id := 3; task_cost := 1; task_period := 6;
                                 task_deadline := 6; task_jitter := 1|}.

    (* Let ts be a task set containing these three tasks, ... *)
    Program Let ts := Build_set [:: tsk1; tsk2; tsk3] _.

    (* ...which can be shown to have valid parameters. *)
    Fact ts_has_valid_parameters:
      valid_sporadic_taskset task_cost task_period task_deadline ts.
    Proof.
      intros tsk IN.
      repeat (move: IN => /orP [/eqP EQ | IN]; subst; compute); by done.
    Qed.

    (* Next, recall the FP RTA schedulability test using RM as the FP policy. *)
    Let RTA_claimed_bounds :=
      fp_claimed_bounds task_cost task_period task_deadline task_jitter (RM task_period).
    Let schedulability_test :=
      fp_schedulable task_cost task_period task_deadline task_jitter (RM task_period).

    (* First, we show that the schedulability test returns the following bounds.
       (Note that although we check the task jitter, these values only include the
        response-time bounds.) *)
    Fact RTA_yields_these_bounds :
      RTA_claimed_bounds ts = Some [:: (tsk1, 2); (tsk2, 2); (tsk3, 3)].
    Proof.
      rewrite /RTA_claimed_bounds /fp_claimed_bounds.
      set RESP := [seq _ | tsk <- ts].
      suff EQ: RESP = [:: (tsk1, Some 2); (tsk2, Some 2); (tsk3, Some 3)].
        by rewrite EQ; compute.
      rewrite /RESP /ts /=; do 2 f_equal.
      {
        rewrite /per_task_rta /=.
        have WORK: total_workload_bound_fp task_cost task_period task_jitter (RM task_period)
                                                 [:: tsk1; tsk2; tsk3] tsk1 1 = 2.
        {
          by compute; rewrite unlock; compute.
        }
        rewrite !WORK /=; clear WORK.
        have WORK: total_workload_bound_fp task_cost task_period task_jitter (RM task_period)
                                                 [:: tsk1; tsk2; tsk3] tsk1 2 = 2.
        {
          by compute; rewrite unlock; compute.
        }
        by rewrite !WORK /=.
      }
      f_equal.
      {
        rewrite /per_task_rta /=.
        have WORK: total_workload_bound_fp task_cost task_period task_jitter (RM task_period)
                                                 [:: tsk1; tsk2; tsk3] tsk2 1 = 2.
        {
          by compute; rewrite unlock; compute.
        }
        rewrite !WORK /=; clear WORK.
        have WORK: total_workload_bound_fp task_cost task_period task_jitter (RM task_period)
                                                 [:: tsk1; tsk2; tsk3] tsk2 2 = 2.
        {
          by compute; rewrite unlock; compute.
        }
        by rewrite !WORK /=.
      }
      do 2 f_equal.
      {
        rewrite /per_task_rta /=.
        have WORK: total_workload_bound_fp task_cost task_period task_jitter (RM task_period)
                                                 [:: tsk1; tsk2; tsk3] tsk3 1 = 3.
        {
          by compute; rewrite unlock; compute.
        }
        rewrite !WORK /=; clear WORK.
        have WORK: total_workload_bound_fp task_cost task_period task_jitter (RM task_period)
                                                 [:: tsk1; tsk2; tsk3] tsk3 3 = 3.
        {
          by compute; rewrite unlock; compute.
        }
        by rewrite !WORK /=; clear WORK.
      }
    Qed.

    (* Since the response-time bounds plus task jitter are no larger than task deadlines,
       the schedulability test indeed returns true. *)
    Fact schedulability_test_succeeds :
      schedulability_test ts = true.
    Proof.
      rewrite /schedulability_test /fp_schedulable -/RTA_claimed_bounds.
      by rewrite RTA_yields_these_bounds.
    Qed.

    (* Now, let's show that the task set is schedulable. *)

    (* Let arr_seq be the periodic arrival sequence from ts... *)
    Let arr_seq := periodic_arrival_sequence ts.

    (* ...subject to rate-monotonic priority. *)
    Let higher_eq_priority := FP_to_JLDP job_task (RM task_period).

    (* Assume that jobs have jitter that is no larger than the jitter of their tasks. *)
     Variable job_jitter: concrete_job -> time.
     Hypothesis H_jitter_is_bounded:
       forall j,
         arrives_in arr_seq j ->
         job_jitter_leq_task_jitter task_jitter job_jitter job_task j.

    (* Next, let sched be the jitter-aware RM schedule with those jitter values. *)
    Let sched := scheduler job_arrival job_cost job_jitter arr_seq higher_eq_priority.

    (* To conclude, based on the definition of deadline miss,... *)
    Let no_deadline_missed_by :=
      task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched.

    (* ...we use the result of the jitter-aware FP RTA to conclude that
       no task misses its deadline. *)
    Corollary ts_is_schedulable:
      forall tsk,
        tsk \in ts ->
        no_deadline_missed_by tsk.
    Proof.
      rename H_jitter_is_bounded into JIT.
      intros tsk IN.
      have VALID := periodic_arrivals_valid_job_parameters ts ts_has_valid_parameters.
      have TSVALID := ts_has_valid_parameters.
      unfold valid_sporadic_job, valid_realtime_job in *; des.
      apply taskset_schedulable_by_fp_rta with (task_cost := task_cost)
                (task_period := task_period) (task_deadline := task_deadline) (ts0 := ts)
                (higher_eq_priority0 := RM task_period) (job_jitter0 := job_jitter)
                (task_jitter := task_jitter); try (by done).
      - by apply periodic_arrivals_are_consistent.
      - by apply periodic_arrivals_is_a_set.
      - by apply periodic_arrivals_all_jobs_from_taskset.
      - by intros j ARRj; specialize (VALID j ARRj); des; repeat split; try (apply JIT).
      - by apply periodic_arrivals_are_sporadic.
      - by apply RM_is_reflexive.
      - by apply RM_is_transitive.
      - by apply scheduler_jobs_come_from_arrival_sequence.
      - by apply scheduler_jobs_execute_after_jitter.
      - by apply scheduler_completed_jobs_dont_execute.
      - by apply scheduler_work_conserving, periodic_arrivals_are_consistent.
      - apply scheduler_respects_policy; first by apply periodic_arrivals_are_consistent.
        -- by intros t; apply RM_is_transitive.
        -- intros j1 j2 t ARR1 ARR2; apply leq_total.
      - by apply schedulability_test_succeeds.
    Qed.

  End ExampleRTA.

End ResponseTimeAnalysisFP.

author: cd-public

repo: rt-proofs

save_path: github-repos/coq/cd-public-rt-proofs


text:
(*
  Copyright (c) 2018, Inria, CEA, Northern Arizona University.
  All rights reserved.

  Redistribution and use in source and binary forms, with or without
  modification, are permitted provided that the following conditions
  are met:
  1. Redistributions of source code must retain the above copyright
     notice, this list of conditions and the following disclaimer.
  2. Redistributions in binary form must reproduce the above copyright
     notice, this list of conditions and the following disclaimer in the
     documentation and/or other materials provided with the distribution.
  3. Neither the name of the Institute nor the names of its contributors
     may be used to endorse or promote products derived from this software
     without specific prior written permission.

  THIS SOFTWARE IS PROVIDED BY THE INSTITUTE AND CONTRIBUTORS ``AS IS'' AND
  ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
  IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
  ARE DISCLAIMED.  IN NO EVENT SHALL THE INSTITUTE OR CONTRIBUTORS BE LIABLE
  FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
  DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
  OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
  HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
  OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
  SUCH DAMAGE.

  This file is part of the verification of the Contiki operating system.

  Authors: - Allan Blanchard <mail@allan-blanchard.fr>
           - Nikolai Kosmatov <nikolai.kosmatov@cea.fr>
           - Frédéric Loulergue <frederic.loulergue@nau.edu>
*)

(* ---------------------------------------------------------- *)
(* --- Lemma 'n_plus_1th_next'                            --- *)
(* ---------------------------------------------------------- *)
Require Import ZArith.
Require Import Reals.
Require Import BuiltIn.
Require Import int.Int.
Require Import int.Abs.
Require Import int.ComputerDivision.
Require Import real.Real.
Require Import real.RealInfix.
Require Import real.FromInt.
Require Import map.Map.
Require Import Qedlib.
Require Import Qed.

(* --- Global Definitions (continued #2) --- *)
Require Import Memory.
Require Import Vlist.

Require Import Axiomatic1.
Require Import Compound.

Hypothesis Q_linked_ll_end: forall (t : array Z),
  forall (t_1 : farray addr addr), forall (l : (list addr)),
  forall (a_1 a : addr), ((nil) <> l) -> ((P_linked_ll t t_1 a_1 a l)) ->
  ((t_1.[ (shiftfield_F1_list_next ((nth l (((length l))%Z - 1%Z)%Z))) ]) =
   a).

Require Import Axiomatic.

Hypothesis Q_separated_linked_ll_append: forall (t : array Z),
  forall (t_1 : farray addr addr), forall (l : (list addr)),
  forall (a_1 a : addr), let a_2 := t_1.[ (shiftfield_F1_list_next a) ] in
  ((valid_rw t a 2%Z)) -> ((P_ptr_separated_from_list a_2 l)) ->
  ((P_linked_ll t t_1 a_1 a l)) -> ((separated a 2%Z a_2 2%Z)) ->
  ((P_linked_ll t t_1 a_1 a_2 ((concat l (cons a nil))))).

Hypothesis Q_inversion_linked_ll: forall (t : array Z),
  forall (t_1 : farray addr addr), forall (l : (list addr)),
  forall (a_1 a : addr), ((P_linked_ll t t_1 a_1 a l)) ->
  (((a_1 = a) /\ ((nil) = l)) \/
   (exists l_1 : (list addr), (a_1 <> a) /\
    (((cons a_1 (concat l_1 nil))) = l) /\
    ((P_ptr_separated_from_list a_1 l_1)) /\ ((valid_rw t a_1 2%Z)) /\
    ((separated a_1 2%Z a 2%Z)) /\
    ((P_linked_ll t t_1 (t_1.[ (shiftfield_F1_list_next a_1) ]) a l_1)))).

Hypothesis Q_dptr_separated_concat: forall (l_1 l : (list addr)),
  forall (a : addr),
  (((P_dptr_separated_from_list a l)) /\
   ((P_dptr_separated_from_list a l_1))) <->
  ((P_dptr_separated_from_list a ((concat l_1 (concat l nil))))).

Hypothesis Q_dptr_separated_from_cons: forall (l : (list addr)),
  forall (a_1 a : addr),
  (((P_dptr_separated_from_list a_1 l)) /\ ((separated a 2%Z a_1 1%Z))) <->
  ((P_dptr_separated_from_list a_1 ((cons a (concat l nil))))).

Hypothesis Q_dptr_separated_from_nil: forall (a : addr),
  (P_dptr_separated_from_list a (nil)).

Hypothesis Q_ptr_separated_concat: forall (l_1 l : (list addr)),
  forall (a : addr),
  (((P_ptr_separated_from_list a l)) /\ ((P_ptr_separated_from_list a l_1))) <->
  ((P_ptr_separated_from_list a ((concat l_1 (concat l nil))))).

Hypothesis Q_ptr_separated_from_cons: forall (l : (list addr)),
  forall (a_1 a : addr),
  (((P_ptr_separated_from_list a_1 l)) /\ ((separated a 2%Z a_1 2%Z))) <->
  ((P_ptr_separated_from_list a_1 ((cons a (concat l nil))))).

Hypothesis Q_ptr_separated_from_nil: forall (a : addr),
  (P_ptr_separated_from_list a (nil)).

Hypothesis Q_in_list_in_sublist: forall (l_1 l : (list addr)),
  forall (a : addr), (((P_in_list a l)) \/ ((P_in_list a l_1))) <->
  ((P_in_list a ((concat l_1 (concat l nil))))).

Goal
  forall (t : array Z),
  forall (t_1 : farray addr addr),
  forall (l : (list addr)),
  forall (a_1 a : addr),
  ((P_linked_ll t t_1 a_1 a l)) ->
  (forall (i : Z), ((0 <= i)%Z) -> (((2 + i) <= ((length l)))%Z) ->
   ((t_1.[ (shiftfield_F1_list_next ((nth l i%Z))) ]) =
    ((nth l (1%Z + i%Z)%Z)))).

Proof.
  intros Mi Ma ll bl el NoDup.
  induction NoDup ; intros i Li Hi.
  + rewrite length_nil in Hi ; omega.
  + subst.
    inversion NoDup ; subst.
    - rewrite Vlist.length_cons in Hi.
      rewrite rw_nil_concat_right in Hi.
      subst.
      rewrite length_nil in Hi ; omega.
    - assert(Cases: i = 0 \/ 0 < i) by omega.
      inversion_clear Cases as [ Eq | Neq ] ; subst.
      * repeat(rewrite rw_nil_concat_right).
        unfold nth ; simpl ; auto.
      * repeat(rewrite rw_nil_concat_right).
        repeat(rewrite rw_nil_concat_right in IHNoDup).
        replace (nth (cons a_1 (cons (t_1 .[ shiftfield_F1_list_next a_1]) l0)) i)
           with (nth (cons (t_1 .[ shiftfield_F1_list_next a_1]) l0) (i-1))
             by (symmetry ; apply Vlist.nth_cons ; omega).
        replace (nth (cons a_1 (cons (t_1 .[ shiftfield_F1_list_next a_1]) l0)) (1 + i))
           with (nth (cons (t_1 .[ shiftfield_F1_list_next a_1]) l0) (1 + (i - 1))).
        ++ apply IHNoDup ; try omega.
           repeat(rewrite rw_nil_concat_right in Hi).
           repeat(rewrite Vlist.length_cons in Hi).
           repeat(rewrite Vlist.length_cons).
           omega.
        ++ replace (1 + (i - 1)) with ((1 + i) - 1) by omega.
           symmetry ; apply Vlist.nth_cons ; omega.
Qed.

author: mriiad

repo: queue

save_path: github-repos/coq/mriiad-queue


text:
(** Generated by coq-of-ocaml *)
Require Import OCaml.OCaml.

Local Set Primitive Projections.
Local Open Scope string_scope.
Local Open Scope Z_scope.
Local Open Scope type_scope.
Import ListNotations.

Unset Positivity Checking.
Unset Guard Checking.

Inductive nat : Set :=
| O : nat
| S : nat -> nat.

Inductive natural : Set :=
| Zero : natural
| Succ : natural -> natural.

Fixpoint plus (plus_arg0 : natural) (plus_arg1 : natural) {struct plus_arg0}
  : natural :=
  match plus_arg0 with
  | Zero => plus_arg1
  | Succ n => Succ (plus n plus_arg1)
  end.

Fixpoint mult (mult_arg0 : natural) (mult_arg1 : natural) {struct mult_arg0}
  : natural :=
  match mult_arg0 with
  | Zero => Zero
  | Succ n => plus (mult n mult_arg1) mult_arg1
  end.

Definition synth (lf1 : natural) (y : natural) (z : natural) (lf2 : natural)
  : natural := plus lf1 (mult Zero lf2).

author: yalhessi

repo: lemmaranker

save_path: github-repos/coq/yalhessi-lemmaranker


text:
(* week-02_the-revert-tactic.v *)
(* FPP 2020 - YSC3236 2020-2021, Sem1 *)
(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
(* Version of 23 Aug 2020 *)

(* ********** *)

Lemma a_proposition_implies_itself :
  forall A : Prop,
    A -> A.
Proof.
  intro A.
  intro H_A.
  exact H_A.

  Restart.

  intro A.
  intro H_A.
  revert H_A.    (* <-- *)
  revert A.      (* <-- *)
  intros A H_A.
  exact H_A.
Qed.

(* ********** *)

Lemma swapping_the_order_of_quantifiers :
  forall A B : Prop,
    (A -> B -> A /\ B) -> B -> A -> A /\ B.
Proof.
  intros A B H_implication H_B H_A.
  exact (H_implication H_A H_B).

  Restart.

  intros A B H_implication H_B H_A.
  revert H_B.
  revert H_A.
  exact H_implication.

  Restart.

  intros A B H_implication H_B H_A.
  revert H_B.
  revert H_A.
  revert H_implication.
  exact (a_proposition_implies_itself (A -> B -> A /\ B)).
Qed.

(* ********** *)

(* end of week-02_the-revert-tactic.v *)

author: soedirgo

repo: fpp

save_path: github-repos/coq/soedirgo-fpp


text:
(* Functional and dependently typed programming *)

Axiom todo : forall {A}, A.

(* Let's have a look at vectors again. *)

Inductive vec (A : Type) : nat -> Type :=
| vnil : vec A 0
| vcons (a : A) (n : nat) (v : vec A n) : vec A (S n).

Arguments vnil {_}.
Arguments vcons {_} _ {_}.

(* You can write the head and tail functions without needing a default case. *)
(* Let's think about how we would do it on paper first. *)

Definition head {A n} (v : vec A (S n)) : A :=
  match v with
  |vcons a n0 => a
  end.

  Print IDProp.
  Print idProp.
  Print head.

Definition tail {A n} (v : vec A (S n)) : vec A n :=
  match v with
  |vcons a t => t
  end.

(* Coq is not always smart enough to see that some patterns are impossible.
  Consider the following zip function. How can you actually define it?
*)

Fail Fixpoint zip {A B n} (v : vec A n) (v' : vec B n) : vec (A * B) n :=
  match v, v' with
  | vnil, vnil => vnil
  | vcons a v, vcons b v' => vcons (a, b) (zip v v')
  end.

Fixpoint zip' {A B n} (v : vec A n) (v' : vec B n) : vec (A * B) n :=
  match v as w in vec _ m
  return
    vec B m -> vec (A * B) m
  with
  | vnil => fun v' => vnil
  | vcons a v => fun v' => vcons (a,head v') (zip' v (tail v'))
    end v'
  .

(* Are you satisfied when comparing to the ideal zip above? *)

(* Equations lets us deal with dependent pattern matching nicely. *)

From Equations Require Import Equations.

Equations zip {A B n} (v : vec A n) (v' : vec B n) : vec (A * B) n :=
  zip vnil vnil := vnil ;
  zip (vcons a v) (vcons b v') := vcons (a, b) (zip v v').

(* We can also define a function for accessing elements. *)
(* We can use bounded natural numbers to do it. *)

Inductive fin : nat -> Type :=
| fin0 n : fin (S n)
| finS n (x : fin n) : fin (S n).

Arguments fin0 {n}.
Arguments finS {n}.

Equations vnth {A n} (v : vec A n) (x : fin n) : A :=
  vnth (vcons a v) (fin0) := a;
  vnth (vcons _ v') (finS x) := vnth v' x.

(* We can now prove that zip and vnth commute. *)

(* To prove it without using too much Equations facilities we can prove first
  the following lemma.
*)

Lemma vec_expand :
  forall A n (v : vec A (S n)),
    v = vcons (head v) (tail v).
Proof.
  intros.
  refine match v with |vcons a v' => _ end.
  reflexivity.
Qed.

(* We will need simp from Equations because by default Equations definitions are opaque.
  simp vnth for instance will apply simplications of the vnth function.
*)

Lemma zip_vnth_by_hand :
  forall A B n (v : vec A n) (v' : vec B n) (x : fin n),
    vnth (zip v v') x = (vnth v x, vnth v' x).
Proof.
  intros.
  induction x.
  - erewrite vec_expand with (v:= v).
    erewrite vec_expand with (v:= v').
    simp zip vnth.
    reflexivity.
  - erewrite vec_expand with (v:= v).
    erewrite vec_expand with (v:= v').
    simp zip vnth.
Qed.

(* Using dependent elimination we don't need the extra lemma.
  It works a bit like destruct but instead of giving names for the variables
  you give patterns directly. For lists you would have for instance
  dependent elimination l as [ nil | x :: r ].
  This uses Equations's machinery so you can actually remove inaccessible
  patterns like we did for zip or vnth.
*)

Lemma zip_vnth_without_funelim :
  forall A B n (v : vec A n) (v' : vec B n) (x : fin n),
    vnth (zip v v') x = (vnth v x, vnth v' x).
Proof.
  intros.
  induction x.
  - dependent elimination v.
    dependent elimination v'.
    simp zip vnth.
    reflexivity.
  - dependent elimination v.
    dependent elimination v'.
    simp zip vnth.
Qed.

(* We can also use the funelim tactic to do the case disjunction for us. *)

Derive Signature NoConfusion NoConfusionHom for fin.
Derive NoConfusion for vec.

Lemma zip_vnth :
  forall A B n (v : vec A n) (v' : vec B n) (x : fin n),
    vnth (zip v v') x = (vnth v x, vnth v' x).
Proof.
  intros A B n v v' x.
  funelim (vnth v x). (* Notice how both v and x are destructed at once. *)
  - funelim (vnth v' _).
    simp zip vnth. reflexivity.
  - funelim (vnth v'0 _).
    simp zip vnth.
  (* Well, this only works if you have defined vnth properly. *)
Qed.

(* How does this work? *)
Search zip. (* You will see many properties that were automatically proven. *)
(* They are used by simp and funelim. *)
(* For instance we could use zip_equation_2 to rewrite by hand. *)

(* These equations can also be found in the graph. *)
Print zip_graph.
Check zip_graph_correct.

(* We can also use notations within Equations definitions *)

Reserved Notation "x +++ y" (at level 60, right associativity).

Equations vapp {A n m} (v : vec A n) (v' : vec A m) : vec A (n + m) := {
  vnil +++ v' := v' ;
  vcons a v +++ v' := vcons a (v +++ v')
} (* Note the need for braces. *)
where "x +++ y" := (vapp x y).

(* Stating associativity however is going to be a problem. *)
Fail Lemma vapp_assoc :
  forall A n m k (v1 : vec A n) (v2 : vec A m) (v3 : vec A k),
    v1 +++ v2 +++ v3 = (v1 +++ v2) +++ v3.

(* To state it we need to use the face that addition is associative. *)
(* To leverage this we use the notion of transport: *)

Definition transport {A} {P : A -> Type} {u v} (e : u = v) : P u -> P v :=
  match e with
  | eq_refl => fun x => x
  end.

From Coq Require Import Lia.

Search ((_ + _) + _).

(* Using the Search command above you should be able to find a replacement
  for todo in the statement.
*)

Lemma vapp_assoc :
  forall A n m k (v1 : vec A n) (v2 : vec A m) (v3 : vec A k),
    v1 +++ v2 +++ v3 =
    transport (todo) ((v1 +++ v2) +++ v3).
Proof.
  (* Do you manage to do the proof? Try a bit to see the problem, if any. *)
  intros.

Abort.

(* To help fix the problem we will assume uniqueness of identity proofs. *)
(* Note that we do not actually need it. See project. *)

Axiom K : forall A (u : A) (e : u = u), e = eq_refl.

(* From it we can eliminate useless transport *)
Lemma transportK :
  forall A (u : A) (e : u = u) (P : A -> Type) (t : P u),
    transport e t = t.
Proof.
Admitted.

(* Now prove that transport commutes with vcons *)
Lemma transport_vcons :
  forall A n m e e' a (v : vec A n),
    transport e (vcons a v) = vcons a (n := m) (transport e' v).
Proof.
Admitted.

(* Let's try again *)

Lemma vapp_assoc :
  forall A n m k (v1 : vec A n) (v2 : vec A m) (v3 : vec A k),
    v1 +++ v2 +++ v3 =
    transport (todo) ((v1 +++ v2) +++ v3).
Proof.
Admitted.

(* The proof is actually doable but we see here that this is a pain. *)

(* Worse, these transports will pollute terms as well.
  Try to fix the rev_acc definition below.

  Note, you can leave underscores (_) in places you want to leave for later.
  You can use Equations? (with a question mark) to open a goal with the missing
  information to fill (proof obligations).
  Equations might solve them automatically. I recommend to use
  #[tactic=idtac] Equations?
  first, in order to see what it must solve.
*)

Fail Equations rev_acc {A n m} (v : vec A n) (acc : vec A m) : vec A (n + m) :=
  rev_acc vnil acc := acc ;
  rev_acc (vcons a v) acc := rev_acc v (vcons a acc).

(* A more practical approach to vectors is the use of subset types: *)

From Coq Require Import List.
Import ListNotations.

Definition ilist (A : Type) (n : nat) :=
  { l : list A | length l = n }.

(* Some notation so that it's nicer (feel free to change it if you don't like
  unicode or whatever).
*)
Notation "⟨ u | v ⟩" := (exist _ u v) (at level 0).

(* This "only parsing" notation is just to avoid writing an underscore
  when writing functions.
*)
Notation "⟨ u ⟩" := (⟨ u | _ ⟩) (at level 0, only parsing).

(* One lemma about equality on this structure *)

Lemma ilist_eq :
  forall A n (l l' : ilist A n),
    proj1_sig l = proj1_sig l' ->
    l = l'.
Proof.
  intros A n [l e] [l' e'] H.
  simpl in H.
  subst l'.
  f_equal.
  (* Note that besides rewrite, you can use subst x to substitute x by u
    when you have an hypothesis of the form x = u or u = x. *)
Admitted.

Definition to_ilist {A} (l : list A) : ilist A (length l) :=
  todo
.

(* We can show that they are equivalent to our other notion of vectors. *)
(* For this we simply say that there is a bijection between the two. *)

Record equiv (A B : Type) := {
  l_to_r : A -> B ;
  r_to_l : B -> A ;
  l_to_l : forall a, r_to_l (l_to_r a) = a ;
  r_to_r : forall b, l_to_r (r_to_l b) = b
}.

(* Don't hesitate to write auxiliary functions to help you. *)

Lemma equiv_ilist :
  forall A n,
    equiv (vec A n) (ilist A n).
Proof.
  intros A n.
  (* Showing you what you can do to give the equivalence nicely. *)
  (* The notation 'p lets you perform a match on the fly (when there is only one
    constructor)
  *)
  unshelve refine {|
    l_to_r v := todo ;
    r_to_l '⟨ l | e ⟩ := todo
  |}.
  - apply todo.
  - apply todo.
Defined.

(* Let's write the head function on ilist *)
Equations hd {A n} (l : ilist A (S n)) : A :=
  hd l := todo.

(* And tail. *)
Equations tl {A n} (l : ilist A (S n)) : ilist A n :=
  tl l := todo.

(* We can do append again. *)
Reserved Notation "x ⊕ y" (at level 60, right associativity).

Equations? iapp {A n m} (l : ilist A n) (l' : ilist A m) : ilist A (n + m) := {
  ⟨ l | e ⟩ ⊕ ⟨ l' | e' ⟩ := ⟨ l ++ l' ⟩
}
where "x ⊕ y" := (iapp x y).
Proof.
Admitted.

(* Wait, associativity still suffers from the same problem! *)
Fail Lemma iapp_assoc :
  forall A n m k (v1 : ilist A n) (v2 : ilist A m) (v3 : ilist A k),
    v1 ⊕ v2 ⊕ v3 = (v1 ⊕ v2) ⊕ v3.

(* The rationale here is: we don't care! We have ilist_eq that says that
  only equality of the underlying lists matters. We separate the data from
  its invariants (length).
*)

(* We can also write the nth function on ilist. *)
(* Notice how, Equations here will not figure out everything and we have to
  help it see that some cases are impossible using False_rect _ _.
*)

Equations? inth {A n} (l : ilist A n) (x : fin n) : A :=
  inth l x := todo.
Proof.
Qed.

(* Let's switch subjects a bit now. *)

(* Before, let's adjust one Equations setting. *)
Set Equations Transparent.
(* It simply says that Equations definition shouldn't be opaque anymore.
  They will behave like regular functions. This means we don't always need
  to use simp to simplify things.
*)

(* Simply typed λ-calculus *)
(* We will use dependent types to define well-typed syntax. *)

(* We define our simple types. *)
(* If it's too easy for you, you can add more stuff like pairs. *)
Inductive type := tunit | tarrow (a b : type).

Notation "A ⇒ B" := (tarrow A B) (at level 20, right associativity).

(* Open terms can have variables. We store their types in an environment. *)
(* We use vectors so it's easy to keep track of variables. *)
(* We could use lists as well. *)
Definition env := vec type.

Inductive term {n} (Γ : env n) : type -> Type :=
| tvar (x : fin n) : term Γ (vnth Γ x)
| tstar : term Γ tunit
| tlam (A : type) B (b : term (vcons A Γ) B) : term Γ (tarrow A B)
| tapp A B (f : term Γ (tarrow A B)) (u : term Γ A) : term Γ B.

Arguments tvar {n Γ}.
Arguments tstar {n Γ}.
Arguments tlam {n Γ} _ {B}.
Arguments tapp {n Γ A B}.

(* You can write your examples. Sometimes you need to give the shape of the
  context to Coq so it can figure out the length. This is annoying, but
  unification is not complete.

  Notice you can only write well-typed terms by construction.
*)

(* The example below needs some definitions above to be completed to work.
  Once that is done you should be able to safely remove the Fail.
*)
 Example test A B : term vnil _ :=
  tlam (A ⇒ B) (tlam A (tapp (tvar (Γ := vcons _ (vcons _ _)) (finS fin0)) (tvar fin0))).

(* This one is supposed to fail. *)
Fail Example test' : term vnil _ :=
  tapp tstar tstar.

(* Let us now "interpret" these terms and types into Coq (Gallina) terms. *)

(* We have to start with types, we need to give a meaning (interpretation) to
  tunit and tarrow. There should be nothing surprising with how we define them.
*)

Reserved Notation "⟦ A '⟧ty'".

Fixpoint interp_type (t : type) : Type :=
  match t with
  | tunit => unit
  | A ⇒ B => ⟦ A ⟧ty -> ⟦ B ⟧ty
  end

where "⟦ A '⟧ty'" := (interp_type A).

Eval compute in ⟦ (tunit ⇒ tunit) ⇒ tunit ⟧ty.

(* When interpreting terms, we soon see that we need to interpret variables
  somehow. For this we carry around a valuation for our environment Γ.
  It maps every variable (index) to a value of the corresponding type.
*)

Definition valuation {n} (Γ : env n) :=
  forall x, ⟦ vnth Γ x ⟧ty.

(* The empty valuation *)
Definition ρ₀ : valuation vnil :=
  fun x => match x with end.

(* Extension of a valuation with a new value. *)
Equations extend {n Γ A} (ρ : valuation (n := n) Γ) (a : ⟦ A ⟧ty) : valuation (vcons A Γ) :=
extend ρ a (fin0) := a;
extend ρ a (finS x) := ρ x.

(* We are now ready to interpret terms! *)

Reserved Notation "⟦ t | r '⟧tm'".

Equations interp {n Γ A} (t : term (n := n) Γ A) (ρ : valuation Γ) : ⟦ A ⟧ty := {
  ⟦ tstar | ρ ⟧tm := tt;
  ⟦ tvar x | ρ ⟧tm := ρ x;
  ⟦ tlam a b | ρ ⟧tm := fun x => ⟦ b | extend ρ x ⟧tm;
  ⟦ tapp a b | ρ ⟧tm := ⟦ a | ρ ⟧tm ⟦ b | ρ ⟧tm
}
where "⟦ t | r '⟧tm'" := (interp t r).

(* We can test on a few examples and see them get normalised. *)
(* Remove Fail when you reach this. *)

 Eval compute in ⟦ test tunit tunit | ρ₀ ⟧tm.

 Eval compute in ⟦ tapp (test _ _) (test tunit tunit) | ρ₀ ⟧tm.

(* Let us move to another (but similar) notion of evaluation. *)
(* We cosnider monoids and their equational theory.
  Like how simply typed λ-calculus has β-reduction, monoids are associative.

  We will use so-called "free monoids" ie monoids with no extra structure.
  The type monoid A V below contains values in A, variables in V, a neutral
  element ε and a monoid operation _ ⋅ _.
*)

Inductive monoid (A V : Type) :=
| mvar (x : V)
| matom (a : A)
| memp
| mop (u v : monoid A V).

Arguments mvar {A V}.
Arguments matom {A V}.
Arguments memp {A V}.
Arguments mop {A V}.

Notation "'ε'" := (memp).
Notation "u ⋅ v" := (mop u v) (at level 60, right associativity).

(* We will use string for variables in our examples *)
From Coq Require Import String.

Example ex1 : monoid nat string :=
  ((mvar "x" ⋅ matom 3) ⋅ ε ⋅ (mvar "y" ⋅ matom 7))%string.

Example ex2 : monoid nat string :=
  (mvar "x" ⋅ matom 3 ⋅ mvar "y" ⋅ matom 7)%string.

(* Like we did for λ-calculus, we can evaluate these expressions by giving
  an interpretation to variables and obtaining values of type list A.
  Indeed, once you eliminate variables, and up-to associativity, these are
  the only inhabitants of the free monoid.
*)

Definition mvaluation A V := V -> list A.

(* Define the following interpretation using the ++ operator on lists. *)
Fixpoint simpl_eval {A V} (e : monoid A V) (ρ : mvaluation A V) : list A :=
  todo.

(* For our examples, we can use the following valuation. *)
(* It's not very efficient, but it suffices for us. *)

Example myval : mvaluation nat string :=
  fun x =>
    match x with
    | "x" => [ 0 ; 1 ]
    | "y" => [ 2 ]
    | _ => []
    end%string.

Eval compute in simpl_eval ex1 myval.

(* ex1 and ex2 are the same up-to associativity, so their evaluations are
  equal.
*)
Check eq_refl : simpl_eval ex1 myval = simpl_eval ex2 myval.

(* We said we considered inhabitants of the free monoid modulo associativity.
  For now we can evaluate the term and indeed get that.
  But what if we wanted to do that while keeping uninterpreted variables?
*)

(* We can define this associativity (+ neutral ε) relation. *)

Reserved Notation "u ~ v" (at level 90).

Inductive monoid_eq {A V} : monoid A V -> monoid A V -> Prop :=

(* ε is neutral *)

| m_neutral_l : forall u, ε ⋅ u ~ u

| m_neutral_r : forall u, u ⋅ ε ~ u

(* ⋅ is associative *)

| m_assoc : forall u v w, (u ⋅ v) ⋅ w ~ u ⋅ v ⋅ w

(* Equivalence rules *)

| m_refl : forall u, u ~ u

| m_sym : forall u v, u ~ v -> v ~ u

| m_trans : forall u v w, u ~ v -> v ~ w -> u ~ w

(* Congruence rule *)

| m_cong : forall u u' v v', u ~ u' -> v ~ v' -> u ⋅ v ~ u' ⋅ v'

where "u ~ v" := (monoid_eq u v).

Lemma ex1_eq_ex2 : ex1 ~ ex2.
Proof.
Admitted.

(* Another method would be to be able to normalise expressions in the free
  monoid. For this we use a method called normalisation by evaluation (NbE).

  We begin by writing an evaluation function as before, but this time we don't
  want to interpret variables, so instead, we need to handle them as values.
  We say that we "reflect" variables as values.

  Once we do that evaluation is straightforward and doesn't require any
  valuation.
*)

Definition value A V := list (A + V).

(* To understand what the + above is you can run Locate: *)
Locate "+".
(* You should guess that it is the sum type. *)
Print sum.
(* Now you can see that you inhabit it using inl and inr. *)

Fixpoint eval {A V} (e : monoid A V) : value A V :=
  todo.

(* In order to get back a normal form, we need to be able to turn values
  back into free monoid expressions. This process is called reification.
*)

Fixpoint reify {A V} (v : value A V) : monoid A V :=
  todo.

(* Test it on a few examples. If you see trailing ε, then don't throw away that
  version, we might need it later, but try to define it without trailing ε.
*)

(* Normalisation by evaluation is just the process of evaluating the expression
  and then reifying it back to its original syntax.
*)

Definition nbe {A V} (e : monoid A V) : monoid A V :=
  reify (eval e).

(* We can test it on examples. *)

Eval compute in nbe ex1.

(* ex1 and ex2 indeed have the same normal form! *)
Check eq_refl : nbe ex1 = nbe ex2.

(* We can even prove that it's always the case. *)

Lemma eval_sound :
  forall A V (u v : monoid A V),
    u ~ v ->
    eval u = eval v.
Proof.
Admitted.

Lemma nbe_sound :
  forall A V (u v : monoid A V),
    u ~ v ->
    nbe u = nbe v.
Proof.
Admitted.

Lemma nbe_self :
  forall A V (u : monoid A V),
    u ~ nbe u.
Proof.
Admitted.

Lemma nbe_complete :
  forall A V (u v : monoid A V),
  nbe u = nbe v ->
  u ~ v.
Proof.
Admitted.

(* Now, thanks to this we can decide equality in the monoid much faster! *)

Lemma re_ex1_eq_ex2 : ex1 ~ ex2.
Proof.
Admitted.

(* Now, let's switch subject one last time and go back to well-founded
  recursion. This time using Equations.
*)

(* We can look at the Hardt function. It is defined as follows:

  hardt 0 := 0
  hardt 1 := 1
  hardt n := hardt (n - 1) + hardt (hardt (n-1) - hardt (n-2))      when n > 1

  We can actually prove that this is the identity function.
  In fact we will even need to know this fact to get Equations to accept it.
*)

(* Hint: A useful notation to get out of a subset type. *)
Notation "x .1" := (proj1_sig x) (at level 11).

(* by wf n lt says we do well-founded induction on n using lt (<) as an order. *)
Equations? hardt (n : nat) : todo by wf n lt :=
  hardt n := todo.
Proof.
Defined.

(* If you're brave enough, you can look into a similar function for which
  termination is much harder. :)
*)

(* The McCarthy 91 function is defined as follows:

  m91 n := n - 10                when  n > 100
  m91 n := m91 (m91 (n + 11))    otherwise

  It is it interesting because for n ≤ 100 it actually always produces 91.
  So we could actually write:

  m91 n := n - 10                when  n > 100
  m91 n := 91                    otherwise

  Let's say for the sake of fun that we want to write it as specified.
  This is a tricky exercise.
*)

(* Here are some useful tools for this. *)

From Coq Require Import Arith.

(* This gives us notations like "n <? m" to check whether n < m. *)

(* Inside proofs you might want to use stuff like

  destruct (le_gt_dec n m) as [h | h].

  to decide locally whether n is smaller or bigger than m.
*)

(* The following is a trick to let Equations retain equalities inside a pattern
 matching. Otherwise, we might be missing some information in the obligations.
*)

Definition inspect {A} (a : A) : {b | a = b} :=
  exist _ a eq_refl.

Notation "x 'eq:' p" := (exist _ x p) (only parsing, at level 20).

(* Here is a silly example *)

Equations? foo (n : nat) : { b : bool | n < 27 <-> b = true } :=
  foo n with inspect (n <? 27) := {
  | true eq: e => ⟨ true ⟩
  | false eq: e => ⟨ false ⟩
  }.
Proof.
  (* Notice how we have access to e in the goals. *)
  - split. 1: auto.
    intros _. apply Nat.ltb_lt in e. assumption.
  - split. 2: discriminate.
    intro h. apply Nat.ltb_ge in e. lia.
Qed.

(* One last hint: you will need your own order. *)

Definition lt91 (n m : nat) : Prop :=
  todo.

(* And prove it is well founded. *)

#[local] Instance wf_lt91 : WellFounded lt91.
Proof.
Admitted.

(* Let us define the function now. *)

Equations? m91 (n : nat) : todo by wf n lt91 :=
  m91 n := todo.
Proof.
Defined.

author: sebastienPatte

repo: Coq

save_path: github-repos/coq/sebastienPatte-Coq


text:
Require Import Undecidability.Synthetic.Definitions Undecidability.Synthetic.Undecidability.
Require Import Undecidability.PCP.PCP_undec.
Require Import Undecidability.FOL.Undecidability.FOL.
From Undecidability.FOL.Undecidability.Reductions Require Import PCPb_to_FOL PCPb_to_FOL_intu PCPb_to_FOL_class.

Lemma undecidable_FOLstar_prv_intu : undecidable FOL*_prv_intu.
Proof.
   apply (undecidability_from_reducibility PCPb_undec).
   apply PCPb_to_FOL.prv_red.
Qed.

Lemma undecidable_FOLstar_valid : undecidable FOL*_valid.
Proof.
   apply (undecidability_from_reducibility PCPb_undec).
   apply PCPb_to_FOL.valid_star_red.
Qed.

Lemma undecidable_FOL_valid : undecidable FOL_valid.
Proof.
   apply (undecidability_from_reducibility PCPb_undec).
   apply PCPb_to_FOL.valid_red.
Qed.

Lemma undecidable_FOL_satis : undecidable FOL_satis.
Proof.
  apply (undecidability_from_reducibility PCPb_compl_undec).
  apply satis_red.
Qed.

Lemma undecidable_FOL_valid_intu : undecidable FOL_valid_intu.
Proof.
   apply (undecidability_from_reducibility PCPb_undec).
   apply PCPb_to_FOL_intu.kvalid_red.
Qed.

Lemma undecidable_FOL_prv_intu : undecidable FOL_prv_intu.
Proof.
   apply (undecidability_from_reducibility PCPb_undec).
   apply PCPb_to_FOL_intu.kprv_red.
Qed.

Lemma undecidable_FOL_satis_intu : undecidable FOL_satis_intu.
Proof.
  apply (undecidability_from_reducibility PCPb_compl_undec).
  apply ksatis_red.
Qed.

Lemma undecidable_FOL_prv_class : undecidable FOL_prv_class.
Proof.
   apply (undecidability_from_reducibility PCPb_undec).
   apply PCPb_to_FOL_class.cprv_red.
Qed.

Lemma undecidable_FOLstar_prv_class : undecidable FOL*_prv_class.
Proof.
   apply (undecidability_from_reducibility PCPb_undec).
   exists (fun R => F R). intros R. apply (BPCP_CND R).
Qed.

author: uds-psl

repo: coq-synthetic-incompleteness


text:
From stdpp Require Import finite.
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates.
From iris.prelude Require Import options.

Definition discrete_fun_insert `{EqDecision A} {B : A → ofe}
    (x : A) (y : B x) (f : discrete_fun B) : discrete_fun B := λ x',
  match decide (x = x') with left H => eq_rect _ B y _ H | right _ => f x' end.
Global Instance: Params (@discrete_fun_insert) 5 := {}.

Definition discrete_fun_singleton `{EqDecision A} {B : A → ucmra}
  (x : A) (y : B x) : discrete_fun B := discrete_fun_insert x y ε.
Global Instance: Params (@discrete_fun_singleton) 5 := {}.

Section ofe.
  Context {A : Type} `{Heqdec : !EqDecision A} {B : A → ofe}.
  Implicit Types x : A.
  Implicit Types f g : discrete_fun B.

  Global Instance discrete_funO_ofe_discrete :
    (∀ i, OfeDiscrete (B i)) → OfeDiscrete (discrete_funO B).
  Proof. intros HB f f' Heq i. apply HB, Heq. Qed.

  (** Properties of discrete_fun_insert. *)
  Global Instance discrete_fun_insert_ne x :
    NonExpansive2 (discrete_fun_insert (B:=B) x).
  Proof.
    intros n y1 y2 ? f1 f2 ? x'; rewrite /discrete_fun_insert.
    by destruct (decide _) as [[]|].
  Qed.
  Global Instance discrete_fun_insert_proper x :
    Proper ((≡) ==> (≡) ==> (≡)) (discrete_fun_insert (B:=B) x) := ne_proper_2 _.

  Lemma discrete_fun_lookup_insert f x y : (discrete_fun_insert x y f) x = y.
  Proof.
    rewrite /discrete_fun_insert; destruct (decide _) as [Hx|]; last done.
    by rewrite (proof_irrel Hx eq_refl).
  Qed.
  Lemma discrete_fun_lookup_insert_ne f x x' y :
    x ≠ x' → (discrete_fun_insert x y f) x' = f x'.
  Proof. by rewrite /discrete_fun_insert; destruct (decide _). Qed.

  Global Instance discrete_fun_insert_discrete f x y :
    Discrete f → Discrete y → Discrete (discrete_fun_insert x y f).
  Proof.
    intros ?? g Heq x'; destruct (decide (x = x')) as [->|].
    - rewrite discrete_fun_lookup_insert.
      apply: discrete. by rewrite -(Heq x') discrete_fun_lookup_insert.
    - rewrite discrete_fun_lookup_insert_ne //.
      apply: discrete. by rewrite -(Heq x') discrete_fun_lookup_insert_ne.
  Qed.
End ofe.

Section cmra.
  Context {A : Type} `{Heqdec : !EqDecision A} {B : A → ucmra}.
  Implicit Types x : A.
  Implicit Types f g : discrete_fun B.

  Global Instance discrete_funR_cmra_discrete:
    (∀ i, CmraDiscrete (B i)) → CmraDiscrete (discrete_funR B).
  Proof. intros HB. split; [apply _|]. intros x Hv i. apply HB, Hv. Qed.

  Global Instance discrete_fun_singleton_ne x :
    NonExpansive (discrete_fun_singleton x : B x → _).
  Proof.
    intros n y1 y2 ?; apply discrete_fun_insert_ne; [done|].
    by apply equiv_dist.
  Qed.
  Global Instance discrete_fun_singleton_proper x :
    Proper ((≡) ==> (≡)) (discrete_fun_singleton x) := ne_proper _.

  Lemma discrete_fun_lookup_singleton x (y : B x) : (discrete_fun_singleton x y) x = y.
  Proof. by rewrite /discrete_fun_singleton discrete_fun_lookup_insert. Qed.
  Lemma discrete_fun_lookup_singleton_ne x x' (y : B x) :
    x ≠ x' → (discrete_fun_singleton x y) x' = ε.
  Proof. intros; by rewrite /discrete_fun_singleton discrete_fun_lookup_insert_ne. Qed.

  Global Instance discrete_fun_singleton_discrete x (y : B x) :
    (∀ i, Discrete (ε : B i)) →  Discrete y → Discrete (discrete_fun_singleton x y).
  Proof. apply _. Qed.

  Lemma discrete_fun_singleton_validN n x (y : B x) : ✓{n} discrete_fun_singleton x y ↔ ✓{n} y.
  Proof.
    split; [by move=>/(_ x); rewrite discrete_fun_lookup_singleton|].
    move=>Hx x'; destruct (decide (x = x')) as [->|];
      rewrite ?discrete_fun_lookup_singleton ?discrete_fun_lookup_singleton_ne //.
    by apply ucmra_unit_validN.
  Qed.

  Lemma discrete_fun_singleton_core x (y : B x) :
    core (discrete_fun_singleton x y) ≡ discrete_fun_singleton x (core y).
  Proof.
    move=>x'; destruct (decide (x = x')) as [->|];
      by rewrite discrete_fun_lookup_core ?discrete_fun_lookup_singleton
      ?discrete_fun_lookup_singleton_ne // (core_id_core ∅).
  Qed.

  Global Instance discrete_fun_singleton_core_id x (y : B x) :
    CoreId y → CoreId (discrete_fun_singleton x y).
  Proof. by rewrite !core_id_total discrete_fun_singleton_core=> ->. Qed.

  Lemma discrete_fun_singleton_op (x : A) (y1 y2 : B x) :
    discrete_fun_singleton x y1 ⋅ discrete_fun_singleton x y2 ≡ discrete_fun_singleton x (y1 ⋅ y2).
  Proof.
    intros x'; destruct (decide (x' = x)) as [->|].
    - by rewrite discrete_fun_lookup_op !discrete_fun_lookup_singleton.
    - by rewrite discrete_fun_lookup_op !discrete_fun_lookup_singleton_ne // left_id.
  Qed.

  Lemma discrete_fun_insert_updateP x (P : B x → Prop) (Q : discrete_fun B → Prop) g y1 :
    y1 ~~>: P → (∀ y2, P y2 → Q (discrete_fun_insert x y2 g)) →
    discrete_fun_insert x y1 g ~~>: Q.
  Proof.
    intros Hy1 HP; apply cmra_total_updateP.
    intros n gf Hg. destruct (Hy1 n (Some (gf x))) as (y2&?&?).
    { move: (Hg x). by rewrite discrete_fun_lookup_op discrete_fun_lookup_insert. }
    exists (discrete_fun_insert x y2 g); split; [auto|].
    intros x'; destruct (decide (x' = x)) as [->|];
      rewrite discrete_fun_lookup_op ?discrete_fun_lookup_insert //; [].
    move: (Hg x'). by rewrite discrete_fun_lookup_op !discrete_fun_lookup_insert_ne.
  Qed.

  Lemma discrete_fun_insert_updateP' x (P : B x → Prop) g y1 :
    y1 ~~>: P →
    discrete_fun_insert x y1 g ~~>: λ g', ∃ y2, g' = discrete_fun_insert x y2 g ∧ P y2.
  Proof. eauto using discrete_fun_insert_updateP. Qed.
  Lemma discrete_fun_insert_update g x y1 y2 :
    y1 ~~> y2 → discrete_fun_insert x y1 g ~~> discrete_fun_insert x y2 g.
  Proof.
    rewrite !cmra_update_updateP; eauto using discrete_fun_insert_updateP with subst.
  Qed.

  Lemma discrete_fun_singleton_updateP x (P : B x → Prop) (Q : discrete_fun B → Prop) y1 :
    y1 ~~>: P → (∀ y2, P y2 → Q (discrete_fun_singleton x y2)) →
    discrete_fun_singleton x y1 ~~>: Q.
  Proof. rewrite /discrete_fun_singleton; eauto using discrete_fun_insert_updateP. Qed.
  Lemma discrete_fun_singleton_updateP' x (P : B x → Prop) y1 :
    y1 ~~>: P →
    discrete_fun_singleton x y1 ~~>: λ g, ∃ y2, g = discrete_fun_singleton x y2 ∧ P y2.
  Proof. eauto using discrete_fun_singleton_updateP. Qed.
  Lemma discrete_fun_singleton_update x (y1 y2 : B x) :
    y1 ~~> y2 → discrete_fun_singleton x y1 ~~> discrete_fun_singleton x y2.
  Proof. eauto using discrete_fun_insert_update. Qed.

  Lemma discrete_fun_singleton_updateP_empty x (P : B x → Prop) (Q : discrete_fun B → Prop) :
    ε ~~>: P → (∀ y2, P y2 → Q (discrete_fun_singleton x y2)) → ε ~~>: Q.
  Proof.
    intros Hx HQ; apply cmra_total_updateP.
    intros n gf Hg. destruct (Hx n (Some (gf x))) as (y2&?&?); first apply Hg.
    exists (discrete_fun_singleton x y2); split; [by apply HQ|].
    intros x'; destruct (decide (x' = x)) as [->|].
    - by rewrite discrete_fun_lookup_op discrete_fun_lookup_singleton.
    - rewrite discrete_fun_lookup_op discrete_fun_lookup_singleton_ne //; by apply Hg.
  Qed.
  Lemma discrete_fun_singleton_updateP_empty' x (P : B x → Prop) :
    ε ~~>: P → ε ~~>: λ g, ∃ y2, g = discrete_fun_singleton x y2 ∧ P y2.
  Proof. eauto using discrete_fun_singleton_updateP_empty. Qed.
  Lemma discrete_fun_singleton_update_empty x (y : B x) :
    ε ~~> y → ε ~~> discrete_fun_singleton x y.
  Proof.
    rewrite !cmra_update_updateP;
      eauto using discrete_fun_singleton_updateP_empty with subst.
  Qed.
End cmra.

author: amintimany

repo: iris

save_path: github-repos/coq/amintimany-iris


text:
(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program 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 Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)

(** %\subsection*{ support :  concat\_facts.v }%*)
Set Implicit Arguments.
Unset Strict Implicit.
Require Export concat.
Require Export empty.

Section MAIN.
Variable A : Setoid.
Variable n m : Nat.
Variable v : seq n A.
Variable w : seq m A.

(** - More facts about concatenation *)

Lemma concat_first_part :
 forall (i : Nat) (Hi : i < n) (Hi' : i < n + m),
 (v ++ w) (Build_finiteT Hi') =' v (Build_finiteT Hi) in _.
induction n.
intros.
inversion Hi.
intro.
case i.
unfold concat in |- *.
unfold nat_rect in |- *.
simpl in |- *.
intros.
apply Ap_comp; auto with algebra.
intros.
apply Trans with (hdtl v (Build_finiteT Hi)).
apply Trans with ((hdtl v ++ w) (Build_finiteT Hi')).
apply concat_comp; auto with algebra.
2: apply Ap_comp; auto with algebra.
unfold hdtl in |- *.
apply Trans with ((head v;; Seqtl v ++ w) (Build_finiteT Hi'));
 auto with algebra.
apply Trans with (Seqtl v (Build_finiteT (lt_S_n _ _ Hi))); auto with algebra.
apply Trans with ((Seqtl v ++ w) (Build_finiteT (lt_S_n _ _ Hi')));
 auto with algebra.
Qed.

Hint Resolve concat_first_part: algebra.

Lemma concat_second_part :
 forall (i : Nat) (Hi : i < m) (Hi' : n + i < n + m),
 (v ++ w) (Build_finiteT Hi') =' w (Build_finiteT Hi) in _.
induction n.
intros.
unfold concat in |- *.
unfold nat_rect in |- *.
apply Ap_comp; auto with algebra.
intros.
apply Trans with ((hdtl v ++ w) (Build_finiteT Hi')); auto with algebra.
unfold hdtl in |- *.
apply Trans with ((head v;; Seqtl v ++ w) (Build_finiteT Hi'));
 auto with algebra.
cut (S (c + i) < S (c + m)).
intro.
apply Trans with ((Seqtl v ++ w) (Build_finiteT (lt_S_n _ _ H)));
 auto with algebra.
apply Trans with ((head v;; Seqtl v ++ w) (Build_finiteT H));
 auto with algebra.
replace (S (c + i)) with (S c + i).
assumption.
auto.
Qed.

Hint Resolve concat_second_part: algebra.

Lemma concat_prop_per_part :
 forall P : Predicate A,
 (forall (i : Nat) (Hi : i < n), Pred_fun P (v (Build_finiteT Hi))) ->
 (forall (j : nat) (Hj : j < m), Pred_fun P (w (Build_finiteT Hj))) ->
 forall (k : nat) (Hk : k < n + m), Pred_fun P ((v ++ w) (Build_finiteT Hk)).
induction n.
intros.
unfold concat in |- *; unfold nat_rect in |- *.
apply H0.
intros.
generalize Hk; clear Hk; case k; [ intro Hk | intros k0 Hk0 ].
generalize (lt_O_Sn c); intro Hk'.
apply (Pred_compatible_prf (p:=P)) with (v (Build_finiteT Hk'));
 auto with algebra.
simpl in |- *.
apply Ap_comp; auto with algebra.
generalize (lt_S_n _ _ Hk0); intro Hk0'.
fold (c + m) in Hk0'.
apply (Pred_compatible_prf (p:=P)) with ((Seqtl v ++ w) (Build_finiteT Hk0')).
apply IHc; auto with algebra.
clear Hk0' Hk0 k0 k.
intros.
apply (Pred_compatible_prf (p:=P)) with (v (Build_finiteT (lt_n_S _ _ Hi)));
 auto with algebra.

apply Trans with (Seqtl (v ++ w) (Build_finiteT Hk0')).
apply Sym.
generalize Seqtl_to_seq.
intros.
apply (H1 _ _ (v ++ w) _ Hk0' Hk0).
generalize Seqtl_concat.
intro p.
apply Ap_comp; auto with algebra.
Qed.

Lemma concat_prop_per_element :
 forall P : Predicate A,
 (forall (i : Nat) (Hi : i < n) (Hi' : i < n + m),
  Pred_fun P ((v ++ w) (Build_finiteT Hi'))) ->
 (forall (j : Nat) (Hj : j < m) (Hj' : n + j < n + m),
  Pred_fun P ((v ++ w) (Build_finiteT Hj'))) ->
 forall (k : Nat) (Hk : k < n + m), Pred_fun P ((v ++ w) (Build_finiteT Hk)).
intros.
apply concat_prop_per_part.
intros.
generalize (H i Hi); intro.
apply
 (Pred_compatible_prf (p:=P))
  with ((v ++ w) (Build_finiteT (lt_plus_trans _ _ m Hi))).
apply H1.
apply Sym.
apply concat_first_part.
intros.
cut (n + j < n + m).
intro Hj'.
apply (Pred_compatible_prf (p:=P)) with ((v ++ w) (Build_finiteT Hj'));
 auto with algebra.
auto with arith.
Qed.

Lemma split_to_concat :
 forall vw : seq (n + m) A, sigT (fun a => sigT (fun b => vw =' a ++ b in _)).
clear v w.
induction n.
intros.
exists (empty_seq A).
simpl in vw.
exists vw.
simpl in |- *.
red in |- *.
auto with algebra.

clear n; intros.
generalize (IHc (Seqtl vw)).
intros.
inversion_clear X.
exists (head vw;; x).
inversion_clear X0.
exists x0.
apply Trans with (hdtl vw); auto with algebra.
change (vw =' hdtl vw in seq (S (c + m)) A) in |- *.
apply hdtl_x_is_x.
unfold hdtl in |- *.
apply Trans with (head vw;; x ++ x0); auto with algebra.
change (head vw;; Seqtl vw =' head vw;; (x ++ x0:seq (c + m) A) in _) in |- *.
apply cons_comp; auto with algebra.
apply cons_concat_special with (a := head vw) (v := x) (v' := x0).
Qed.
End MAIN.

Hint Resolve concat_first_part: algebra.
Hint Resolve concat_second_part: algebra.

author: coq-contribs

repo: lin-alg

save_path: github-repos/coq/coq-contribs-lin-alg


text:
Require Import List Bool.

Import ListNotations.

Class DecEq {A : Type} := {
  deq (x y : A) : {x = y} + {x <> y}
}.

Notation "a =? b" := (if deq a b then true else false) (at level 70, no associativity).
Notation "a == b" := (deq a b) (at level 70, no associativity).

Inductive Elem {a : Type} : a -> list a -> Prop :=
  | Here (x : a) (xs : list a) : Elem x (x :: xs)
  | There (x y : a) (xs : list a) (prf : Elem x xs) : Elem x (y :: xs).

Definition Member {a : Type} (xs : list a) :=
  { x : a | Elem x xs }.

Inductive Distinct {A : Type} : list A -> Prop :=
  | Empty : Distinct []
  | Cons (x : A) (xs : list A) : ~(Elem x xs) -> Distinct xs -> Distinct (x :: xs).

Inductive IsSubset {A : Type} : list A -> list A -> Prop :=
  | Same (xs : list A) : Distinct xs -> IsSubset xs xs
  | Prepend (x : A) (xs ys : list A) : ~(Elem x xs) -> IsSubset xs ys -> IsSubset xs (x :: ys).

Definition Subset {a : Type} (xs : list a) :=
  { ys : list a | IsSubset ys xs }.

Definition FinType (A : Type) := { all : list A | forall (x : A), Elem x all }.

Definition enum {A : Type} (fin : FinType A) : list A :=
  match fin with
  | exist _ l _ => l
  end.

Definition FinSubset {A : Type} (xs : list A) (fin : FinType A) := IsSubset xs (enum fin).

Definition ext_eq {A : Type} (xs ys : list A) := forall (x : A), Elem x xs <-> Elem x ys.

Lemma subset_prop :
  forall {A : Type} (xs ys : list A),
    IsSubset xs ys -> forall (x : A), Elem x xs -> Elem x ys.
Proof.
intuition.
induction H.
assumption.
constructor.
intuition.
Qed.

Lemma elem_lemma {a : Type} `{DecEq a} :
  forall (x y : a) (xs : list a), Elem x (y :: xs) -> x <> y -> Elem x xs.
Proof.
intuition.
induction xs.
inversion H0.
contradiction.
intuition.
inversion H0.
contradiction.
assumption.
Qed.

Lemma elem {a : Type} `{DecEq a} (x : a) (xs : list a) : {Elem x xs} + ({~ Elem x xs}).
Proof.
induction xs.
right.
intuition.
inversion H0.
intuition.
constructor.
constructor.
assumption.
induction (x == a0).

left.
rewrite a1.
constructor.
right.
contradict b.
intuition.
exact (elem_lemma x a0 xs b b0).
Qed.

Lemma subset_of_empty_is_empty :
  forall {A : Type} (ys : list A), IsSubset ys [] -> ys = [].
Proof.
intuition.
inversion H.
reflexivity.
Qed.

Lemma prod_eq : forall {A B : Type} {a1 a2 : A} {b1 b2 : B}, a1 = a2 -> b1 = b2 -> (a1,b1) = (a2,b2).
Proof.
intuition.
rewrite H, H0.
reflexivity.
Qed.

Lemma prod_neq : forall {A B : Type} {a1 a2 : A} {b1 b2 : B}, a1 <> a2 \/ b1 <> b2 -> (a1,b1) <> (a2,b2).
Proof.
intuition.
inversion H0.
contradiction.
inversion H0.
contradiction.
Qed.

Instance dec_eq_prod (A B : Type) `(EqA : DecEq A, EqB : DecEq B) : @DecEq (prod A B) :=
  {
    deq x y := match x, y with
               | (a1,b1), (a2,b2) =>
                  match a1 == a2, b1 == b2 with
                  | left aprf, left bprf => left (prod_eq aprf bprf)
                  | _, right bprf => right (prod_neq (or_intror bprf))
                  | right aprf, _ => right (prod_neq (or_introl aprf))
                  end
               end
  }.

Fixpoint pair_with {A B : Type} (a : A) (l2 : list B) : list (A * B) :=
  match l2 with
  | []      => []
  | y :: ys => (a,y) :: pair_with a ys
  end.

Fixpoint cart_prod {A B : Type} (l1 : list A) (l2 : list B) : list (A * B) :=
  match l1  with
  | []      => []
  | x :: xs => pair_with x l2 ++ cart_prod xs l2
  end.

Lemma pair_with_member:
  forall {A B : Type} {l2 : list B} (a : A) {b : B} (prf : Elem b l2),
    Elem (a,b) (pair_with a l2).
Proof.
intuition.
induction l2.
inversion prf.
inversion prf.
simpl.
constructor.
simpl.
constructor.
exact (IHl2 prf0).
Qed.

Lemma elem_append_l : forall {A : Type} (x : A) {l1 l2 : list A}, Elem x l1 -> Elem x (l1 ++ l2).
Proof.
intuition.
induction l1.
inversion H.
inversion H.
simpl.
constructor.
simpl.
constructor.
exact (IHl1 prf).
Qed.

Lemma elem_append_r : forall {A : Type} (x : A) {l1 l2 : list A}, Elem x l2 -> Elem x (l1 ++ l2).
Proof.
intuition.
induction l1.
inversion H.
simpl.
rewrite H1.
assumption.
simpl.
rewrite H1.
assumption.
simpl.
constructor.
assumption.
Qed.

Lemma elem_append_only_second :
  forall {A : Type} {l1 l2 : list A} `{DecEq A} (a : A),
    Elem a (l1 ++ l2) -> ~(Elem a l1) -> Elem a l2.
Proof.
intuition.
induction l1.
simpl in H0.
assumption.
simpl in H0.
inversion H0.
induction l2.
rewrite app_nil_r in H0.
contradiction.
rewrite H4 in H1.
pose proof Here a0 l1.
contradiction.
induction (elem a l1).
pose proof There a a0 l1 a1.
contradiction.
exact (IHl1 prf b).
Qed.

Lemma pair_member :
  forall {A B : Type} {l1 : list A} {l2 : list B} {x : A} {y : B} (a : Elem x l1) (b : Elem y l2),
    Elem (x, y) (cart_prod l1 l2).
Proof.
intuition.
induction l1.
inversion a.

inversion a.
simpl.

exact (elem_append_l (a0,y) (pair_with_member a0 b)).
simpl.
exact (elem_append_r (x,y) (IHl1 prf)).
Qed.

Lemma pair_with_second :
  forall {A B : Type} {l2 : list B}
         (a : A) (b : B), Elem (a,b) (pair_with a l2) -> Elem b l2.
Proof.
intuition.
induction l2.
inversion H.
inversion H.
constructor.
constructor.
exact (IHl2 prf).
Qed.

Lemma cart_prod_empty_is_empty :
  forall {A B : Type} {l1 : list A}, @cart_prod A B l1 [] = [].
Proof.
intuition.
induction l1.
intuition.
simpl.
assumption.
Qed.

Lemma cart_prod_not_empty_if :
  forall {A B : Type} {l1 : list A} {l2 : list B},
    cart_prod l1 l2 <> [] -> l1 <> [] /\ l2 <> [].
Proof.
intuition.
rewrite H0 in H.
simpl in H.
contradiction.
rewrite H0 in H.
rewrite cart_prod_empty_is_empty in H.
contradiction.
Qed.

Lemma cart_prod_not_empty_fi :
  forall {A B : Type} {l1 : list A} {l2 : list B},
     l1 <> [] /\ l2 <> [] -> cart_prod l1 l2 <> [].
Proof.
intuition.
induction l1.
contradiction.
induction l2.
contradiction.
inversion H0.
Qed.

Lemma elem_means_nonempty :
  forall {A : Type} (x : A) (l1 : list A), Elem x l1 -> l1 <> [].
Proof.
intuition.
induction l1.
inversion H.
inversion H0.
Qed.

Lemma pair_with_first :
  forall {A B : Type} {l2 : list B}
         (a a0 : A) (b : B), Elem (a,b) (pair_with a0 l2) -> a = a0.
Proof.
intuition.
induction l2.
inversion H.
inversion H.
reflexivity.
exact (IHl2 prf).
Qed.

Lemma cart_prod_second :
  forall {A B : Type} {l1 : list A} {l2 : list B} `{EqA : DecEq A, EqB : DecEq B}
         (b : B), (exists (a : A), Elem (a,b) (cart_prod l1 l2)) -> Elem b l2.
Proof.
intuition.
induction l1.
inversion H.
inversion H0.
destruct H.
simpl in H.
induction (elem (x,b) (pair_with a l2)).
pose proof @pair_with_first A B l2 x a b a0.
rewrite H0 in a0.
exact (pair_with_second a b a0).

pose proof elem_append_only_second (x,b) H b0.
exact (IHl1 (ex_intro _ x H0)).
Qed.

Lemma pair_with_first_contra :
  forall {A B : Type} {l2 : list B} `{DecEq A}
    (a a0 : A) (b : B), a <> a0 -> ~(Elem (a,b) (pair_with a0 l2)).
Proof.
intuition.
induction l2.
inversion H1.
simpl in H1.
inversion H1.
contradiction.
exact (IHl2 prf).
Qed.

Lemma member_cart_prod :
  forall {A B : Type} {l1 : list A} {l2 : list B} `{EqA : DecEq A, EqB : DecEq B}
         (x : A * B), Elem x (cart_prod l1 l2) ->
    match x with
    | (a,b) => Elem a l1 /\ Elem b l2
    end.
Proof.
intuition.
induction l1.
inversion H.
destruct x.
inversion H.
induction (a0 == a).
rewrite a1.
split.
constructor.
exact (cart_prod_second b (ex_intro _ a0 H)).

pose proof @pair_with_first_contra A B l2 EqA a0 a b b0.
pose proof dec_eq_prod A B EqA EqB.
pose proof elem_append_only_second (a0, b) H H1.
constructor.
pose proof IHl1 H3.
intuition.
constructor.
assumption.
exact (cart_prod_second b (ex_intro _ a0 H)).

split.
simpl in H.
induction (a0 == a).
rewrite a1.
constructor.
pose proof @pair_with_first_contra A B l2 EqA a0 a b b0.
pose proof dec_eq_prod A B EqA EqB.
pose proof elem_append_only_second (a0, b) H H1.
constructor.
pose proof IHl1 H3.
intuition.
exact (cart_prod_second b (ex_intro _ a0 H)).
Qed.
(*
Lemma cart_prod_of_subset :
  forall {A B : Type} {l1 : list A} {l2 : list B} `{EqA : DecEq A, EqB : DecEq B}
         (s1 : Subset l1) (s2 : Subset l2),
          match s1, s2 with
          | exist _ l1' _, exist _ l2' _ =>
              forall (a : A) (b : B), Elem (a,b) (cart_prod l1' l2') -> Elem (a,b) (cart_prod l1 l2)
          end.
Proof.
intuition.
destruct s1. destruct s2.
intuition.
destruct (member_cart_prod (a,b) H).
destruct i. destruct i0.
exact (pair_member (H3 a H0) (H5 b H1)).
Qed.

Definition cart_prod_subset
  {A B : Type} {l1 : list A} {l2 : list B} `{EqA : DecEq A, EqB : DecEq B}
  (s1 : Subset l1) (s2 : Subset l2) : list (A * B) :=
  match s1, s2 with
  | exist _ l1' _, exist _ l2' _ => cart_prod l1' l2'
  end. *)

(* Lemma make_subset_prod
  {A B : Type} {l1 : list A} {l2 : list B} `{EqA : DecEq A, EqB : DecEq B}
  (s1 : Subset l1) (s2 : Subset l2) : IsSubset (cart_prod_subset s1 s2) (cart_prod l1 l2).
Proof.
unfold IsSubset.
intuition.
pose proof cart_prod_of_subset s1 s2.
destruct x.
unfold cart_prod_subset in H.
destruct s1. destruct s2.
exact (H0 a b H).
Qed. *)

Lemma empty_has_no_app :
  forall {A : Type} (x : A) (xs : list A),
    xs ++ [x] <> [].
Proof.
intuition.
induction xs.
simpl in H.
discriminate.
inversion H.
Qed.

Lemma app_non_empty :
  forall {A : Type} (xs : list A),
    (exists (x : A) (ys : list A), xs = ys ++ [x])
    <->
    (exists (a : A) (zs : list A), a :: zs = xs).
Proof.
intuition.
induction xs.

destruct H. destruct H.
symmetry in H.
pose proof empty_has_no_app x x0.
contradiction.

exists a. exists xs.
reflexivity.

induction xs.

destruct H. destruct H.
inversion H.

destruct xs.
inversion H.
exists a. exists [].
intuition.
cut (exists (a : A) (zs : list A), a :: zs = a0 :: xs).
intuition. destruct H1. destruct H1.
exists x. exists (a :: x0).
simpl.
rewrite H1.
reflexivity.

exists a0. exists xs.
reflexivity.
Qed.

Lemma pair_with_distinct :
  forall {A B : Type} (x : A) (ys : list B),
    Distinct ys -> Distinct (pair_with x ys).
Proof.
intuition.
induction ys.
simpl.
constructor.
simpl.
inversion H.
constructor.
contradict H2.
exact (pair_with_second x a H2).
intuition.
Qed.

Lemma prod_of_fin_is_fin :
  forall {A B : Type}, FinType A -> FinType B -> FinType (A * B).
Proof.
intuition.
unfold FinType.
destruct X.
destruct X0.
exists (cart_prod x x0).
intuition.
exact (pair_member (e a) (e0 b)).
Qed.

Lemma map_form :
  forall {A B : Type} {f : A -> B} (xs : list A) (b : B),
    Elem b (map f xs) -> exists (x : A), Elem x xs /\ f x = b.
Proof.
intuition.
induction xs.
inversion H.
simpl in H.
inversion H.
exists a.
intuition.
constructor.
destruct (IHxs prf).
exists x0.
intuition.
constructor.
intuition.
Qed.

Fixpoint powerset {A : Type} (xs : list A) : list (list A) :=
  match xs with
  | []      => [[]]
  | x :: xs => powerset xs ++ map (fun subset => x :: subset) (powerset xs)
  end.

Lemma flat_map_works :
  forall {A B : Type} {f : A -> list B} (xs : list A) (a : A) (b : B),
    Elem a xs -> Elem b (f a) -> Elem b (flat_map f xs).
Proof.
intuition.
induction xs.

inversion H.
simpl.
inversion H.
rewrite <- H3.
exact (elem_append_l b H0).
exact (elem_append_r b (IHxs prf)).
Qed.

Lemma powerset_no_discard :
  forall {A : Type} (x : A) (xs : list A) (ys : list A),
    Elem ys (powerset xs) -> Elem ys (powerset (x :: xs)).
Proof.
intuition.
induction xs.

simpl in H.
inversion H.
simpl.
constructor.
inversion prf.

simpl.
simpl in H.
inversion H.
constructor.

rewrite H2.
apply elem_append_l.
assumption.
Qed.

Lemma powerset_has_empty :
  forall {A : Type} (xs : list A), Elem [] (powerset xs).
Proof.
intuition.
induction xs.

simpl.
constructor.

apply powerset_no_discard.
assumption.
Qed.

Lemma empty_is_subset :
  forall {A : Type} (xs : list A), IsSubset [] xs.
Proof.
intuition.
induction xs.
constructor.
constructor.

constructor.

inversion IHxs.
intuition.
inversion H2.
intuition.
inversion H3.
assumption.
Qed.
(*
Lemma tail_of_subset_is_subset :
  forall {A : Type} (x : A) (xs : list A) (ys : list A),
    IsSubset (x :: xs) ys -> IsSubset xs ys.
Proof.
intuition.
induction xs.
apply empty_is_subset.

inversion H.
constructor.
inversion H0.
assumption.
constructor.
inversion H0.
assumption.
constructor.
intuition.
contradict H0.
constructor.
assumption.
induction ys.
inversion H3.

Qed.

Lemma subset_nonempty_supset_nonempty :
  forall {A : Type} (x : A) (xs : list A) (ys : list A),
    IsSubset (x :: xs) ys -> exists (z : A) (zs : list A), ys = z :: zs.
Proof.
intuition.
induction ys.

pose proof subset_of_empty_is_empty (x :: xs) H.
inversion H0.

exists a.
exists ys.
reflexivity.
Qed.

Lemma map_works :
  forall {A B : Type} {f : A -> B} (x : A) (xs : list A),
    Elem x xs -> Elem (f x) (map f xs).
Proof.
intuition.
induction xs.
inversion H.
simpl.
inversion H.
constructor.
constructor.
exact (IHxs prf).
Qed.

Lemma app_elem :
  forall {A : Type} (l1 l2 : list A) (x : A), Elem x (l1 ++ l2) -> Elem x l1 \/ Elem x l2.
Proof.
intuition.
induction l1.
right.
simpl in H.
assumption.
simpl in H.
inversion H.
left.
constructor.
intuition.
constructor.
constructor.
assumption.
Qed. *)
(*
Lemma powerset_has_all_sets :
  forall {A : Type} (xs : list A) (ys : list A),
    IsSubset ys xs -> Elem ys (powerset xs).
Proof.
intuition.

induction ys.

apply powerset_has_empty.

pose proof IHys (tail_of_subset_is_subset a ys xs H).
unfold IsSubset in H.
intuition.

pose proof H2 a (Here a ys).
inversion H.
simpl.

rewrite <- H4 in H0.
simpl in H0.
apply app_elem in H0.
induction H0.
apply elem_append_r.
apply map_works.
assumption.
apply map_form in H0.
destruct H0.
intuition.
inversion H1.
rewrite <- H6 in H0.
pose proof H0 (Here a x0).
contradiction.

rewrite H4.
unfold powerset.

(* This isn't right because the powerset definition doesn't
   actually produce every sublist, just every subsequence. Fix
   or just *)

simpl.
apply elem_append_r. *)

author: ReedOei

repo: FormalModelsOfComputation


text:
From Categories Require Import Essentials.Notations.
From Categories Require Import Essentials.Types.
From Categories Require Import Essentials.Facts_Tactics.
From Categories Require Import Category.Main.

(**
Fro categories C and C', a functor F : C -> C' consists of an arrow map from
objects of C to objects of C' and an arrow map from arrows of C to arrows of C'
such that an arrow h : a -> b is mapped to (F h) : F a -> F b.

Furthermore, we require functors to map identitiies to identities. Additionally,
the immage of the coposition of two arrows must be the same as composition of
their images.
*)
Record Functor (C C' : Category) : Type :=
{
  (** Object map *)
  FO : C → C';

  (** Arrow map *)
  FA : ∀ {a b}, (a --> b)%morphism → ((FO a) --> (FO b))%morphism;

  (** Mapping of identities *)
  F_id : ∀ c, FA (id c) = id (FO c);

  (** Functor commuting with composition *)
  F_compose : ∀ {a b c} (f : (a --> b)%morphism) (g : (b --> c)%morphism),
      (FA (g ∘ f) = (FA g) ∘ (FA f))%morphism

  (* F_id and F_compose together state the fact that functors are morphisms of
 categories (preserving the structure of categories!)*)
}.

Arguments FO {_ _} _ _.
Arguments FA {_ _} _ _ _ _.
Arguments F_id {_ _} _ _.
Arguments F_compose {_ _} _ {_ _ _} _ _.

Notation "C --> D" := (Functor C D) : functor_scope.

Bind Scope functor_scope with Functor.

Notation "F '_o'" := (FO F) : object_scope.

Notation "F '@_a'" := (@FA _ _ F) : morphism_scope.

Notation "F '_a'" := (@FA _ _ F _ _) : morphism_scope.

Hint Extern 2 => (apply F_id) : core.

Local Open Scope morphism_scope.
Local Open Scope object_scope.

Ltac Functor_Simplify :=
  progress
    (
      repeat rewrite F_id;
      (
        repeat
          match goal with
          | [|- ?F _a ?A = id (?F _o ?x)] =>
            (rewrite <- F_id; (cbn+idtac))
          | [|- (id (?F _o ?x)) = ?F _a ?A] =>
            (rewrite <- F_id; (cbn+idtac))
          | [|- ?F _a ?A ∘ ?F _a ?B = ?F _a ?C ∘ ?F _a ?D] =>
            (repeat rewrite <- F_compose; (cbn+idtac))
          | [|- ?F _a ?A ∘ ?F _a ?B = ?F _a ?C] =>
            (rewrite <- F_compose; (cbn+idtac))
          | [|- ?F _a ?C = ?F _a ?A ∘ ?F _a ?B] =>
            (rewrite <- F_compose; (cbn+idtac))
          | [|- context [?F _a ?A ∘ ?F _a ?B]] =>
            (rewrite <- F_compose; (cbn+idtac))
          end
      )
    )
.

Hint Extern 2 => Functor_Simplify : core.

Section Functor_eq_simplification.

  Context {C C' : Category} (F G : (C --> C')%functor).

  (** Two functors are equal if their object maps and arrow maps are. *)
  Lemma Functor_eq_simplify (Oeq : F _o = G _o) :
    ((fun x y =>
        match Oeq in _ = V return ((x --> y) → ((V x) --> (V y)))%morphism with
          eq_refl => F  @_a x y
        end) = G @_a) -> F = G.
  Proof.
    destruct F; destruct G.
    basic_simpl.
    ElimEq.
    PIR.
    trivial.
  Qed.

  (** Extensionality for arrow maps of functors. *)
  Theorem FA_extensionality (Oeq : F _o = G _o) :
    (
      ∀ (a b : Obj)
        (h : (a --> b)%morphism),
        (
          fun x y =>
            match Oeq in _ = V return
                  ((x --> y) → ((V x) --> (V y)))%morphism
            with
              eq_refl => F  @_a x y
            end
        ) _ _ h = G _a h
    )
    →
    (
      fun x y =>
        match Oeq in _ = V return
              ((x --> y) → ((V x) --> (V y)))%morphism
        with
          eq_refl => F  @_a x y
        end
    ) = G @_a.
  Proof.
    auto.
  Qed.

  (** Fucntor extensionality: two functors are equal of their object maps are
      equal and their arrow maps are extensionally equal. *)
  Lemma Functor_extensionality (Oeq : F _o = G _o) :
    (
      ∀ (a b : Obj) (h : (a --> b)%morphism),
        (
          fun x y =>
            match Oeq in _ = V return
                  ((x --> y) → ((V x) --> (V y)))%morphism
            with
              eq_refl => F  @_a x y
            end
        ) _ _ h = G _a h
    ) → F = G.
  Proof.
    intros H.
    apply (Functor_eq_simplify Oeq); trivial.
    apply FA_extensionality; trivial.
  Qed.

End Functor_eq_simplification.

Hint Extern 2 => Functor_Simplify : core.

Ltac Func_eq_simpl :=
  match goal with
    [|- ?A = ?B :> Functor _ _] =>
    (apply (Functor_eq_simplify A B (eq_refl : A _o = B _o)%object)) +
    (cut (A _o = B _o)%object; [
       let u := fresh "H" in
       intros H;
         apply (Functor_eq_simplify A B H)
         |
    ])
  end.

Hint Extern 3 => Func_eq_simpl : core.

Section Functor_eq.
  Context {C C' : Category} (F G : (C --> C')%functor).

  Lemma Functor_eq_morph (H : F = G) :
    ∃ (H : ∀ x, F _o x = G _o x),
    ∀ x y (h : (x --> y)%morphism),
      match H x in _ = V return (V --> _)%morphism with
         eq_refl =>
         match H y in _ = V return (_ --> V)%morphism with
           eq_refl => F _a h
         end
       end = G _a h.
  Proof.
    exists (equal_f (f_equal FO H)).
    intros x y h.
    destruct H; trivial.
  Qed.

End Functor_eq.

repo: Categories

save_path: github-repos/coq/amintimany-Categories


text:
Load LFindLoad.
From lfind Require Import LFind.
From adtind Require Import goal77.

Set Printing Depth 1000.
Definition lfind_eval  y:=
append (rev y) Nil.

Compute lfind_eval  (Cons Zero (Cons (Succ (Succ Zero)) Nil)).

Compute lfind_eval  (Cons (Succ (Succ (Succ Zero))) (Cons (Succ (Succ (Succ Zero))) (Cons Zero Nil))).

Compute lfind_eval  (Cons (Succ Zero) (Cons Zero Nil)).

Compute lfind_eval  (Cons (Succ (Succ Zero)) Nil).

Compute lfind_eval  (Cons (Succ Zero) (Cons Zero (Cons (Succ Zero) Nil))).

Compute lfind_eval  (Cons (Succ Zero) (Cons (Succ (Succ (Succ Zero))) Nil)).

Compute lfind_eval  (Cons (Succ (Succ (Succ (Succ (Succ Zero))))) Nil).

Compute lfind_eval  (Cons (Succ (Succ Zero)) (Cons Zero Nil)).

Compute lfind_eval  (Cons (Succ (Succ (Succ Zero))) Nil).

Compute lfind_eval  (Cons (Succ Zero) Nil).

Compute lfind_eval  (Cons (Succ (Succ Zero)) (Cons (Succ (Succ Zero)) Nil)).

Compute lfind_eval  (Cons Zero Nil).

Compute lfind_eval  (Cons Zero (Cons (Succ Zero) Nil)).

Compute lfind_eval  (Nil).


text:
(* Small-step semantics *)

(* LICENSE NOTICE

Copyright (c) 2018 The MITRE Corporation.
All Rights Reserved.

This proof script is free software: you can redistribute it and/or
modify it under the terms of the BSD License as published by the
University of California.  See license.txt for details. *)

(** A small-step semantics for annotated terms. *)

Require Import List.
Import List.ListNotations.
Open Scope list_scope.
Require Import PeanoNat Minus Lia Preamble Term_Defs Term.

(** * States *)

Inductive St: Set :=
| stop: Plc -> Evidence -> St
| conf: AnnoTerm -> Plc -> Evidence -> St
| rem: nat -> Plc -> St -> St
| ls: St -> AnnoTerm -> St
| bsl: nat -> St -> AnnoTerm -> Plc -> Evidence -> St
| bsr: nat -> Evidence -> St -> St
| bp: nat -> St -> St -> St.

Fixpoint pl (s:St) :=
  match s with
  | stop p _ => p
  | conf _ p _ => p
  | rem _ p _ => p
  | ls st _ => pl st
  | bsl _ _ _ p _ => p
  | bsr _ _ st => pl st
  | bp _ _ st => pl st
  end.

(** The evidence associated with a state. *)

Fixpoint seval st :=
  match st with
  | stop _ e => e
  | conf t p e => aeval t p e
  | rem _ _ st => seval st
  | ls st t => aeval t (pl st) (seval st)
  | bsl _ st t p e => ss (seval st) (aeval t p e)
  | bsr _ e st => ss e (seval st)
  | bp _ st0 st1 => ss (seval st0) (seval st1)
  end.

(** * Labeled Transition System

    The label in a transition is either an event or [None] when the
    transition is silent.  Notice the use of annotations to provide
    the correct number for each event.  *)

Inductive step: St -> option Ev -> St -> Prop :=
(** Measurement *)

| stasp:
    forall r x p e,
      step (conf (aasp r x) p e)
           (Some (asp_event (fst r) x p e))
           (stop p (aeval (aasp r x) p e))
(** Remote call *)

| statt:
    forall r x p q e,
      step (conf (aatt r q x) p e)
           (Some (req (fst r) p q (unanno x) e))
           (rem (snd r) p (conf x q e))
| stattstep:
    forall st0 ev st1 p j,
      step st0 ev st1 ->
      step (rem j p st0) ev (rem j p st1)
| stattstop:
    forall j p q e,
      step (rem j p (stop q e))
           (Some (rpy (pred j) p q e))
           (stop p e)
(** Linear Sequential Composition *)

| stlseq:
    forall r x y p e,
      step (conf (alseq r x y) p e)
           None
           (ls (conf x p e) y)
| stlseqstep:
    forall st0 ev st1 t,
      step st0 ev st1 ->
      step (ls st0 t) ev (ls st1 t)
| stlseqstop:
    forall t p e,
      step (ls (stop p e) t) None (conf t p e)
(** Branching Sequential Composition *)

| stbseq:
    forall r s x y p e,
      step (conf (abseq r s x y) p e)
           (Some (split (fst r) p))
           (bsl (snd r) (conf x p (splitEv_T_l s e))
                y p (splitEv_T_r s e))
| stbslstep:
    forall st0 ev st1 j t p e,
      step st0 ev st1 ->
      step (bsl j st0 t p e) ev (bsl j st1 t p e)
| stbslstop:
    forall j e e' t p p',
      step (bsl j (stop p e) t p' e')
           None
           (bsr j e (conf t p' e'))

| stbsrstep:
    forall st0 ev st1 j e,
      step st0 ev st1 ->
      step (bsr j e st0) ev (bsr j e st1)
| stbsrstop:
    forall j e p e',
      step (bsr j e (stop p e'))
           (Some (join (pred j) p))
           (stop p (ss e e'))

(** Branching Parallel composition *)

| stbpar:
    forall r s x y p e,
      step (conf (abpar r s x y) p e)
           (Some (Term_Defs.split (fst r) p))
           (bp (snd r)
               (conf x p (splitEv_T_l s e))
               (conf y p (splitEv_T_r s e)))
| stbpstepleft:
    forall st0 st1 st2 ev j,
      step st0 ev st2 ->
      step (bp j st0 st1) ev (bp j st2 st1)
| stbpstepright:
    forall st0 st1 st2 ev j,
      step st1 ev st2 ->
      step (bp j st0 st1) ev (bp j st0 st2)
| stbpstop:
    forall j p e p' e',
      step (bp j (stop p e) (stop p' e'))
           (Some (join (pred j) p'))
           (stop p' (ss e e')).
#[export] Hint Constructors step : core.

(** A step preserves place. *)

Lemma step_pl_eq:
  forall st0 ev st1,
    step st0 ev st1 -> pl st0 = pl st1.
Proof.
  intros.
  induction H; simpl; auto.
Qed.

(** A step preserves evidence. *)

Lemma step_seval:
  forall st0 ev st1,
    step st0 ev st1 ->
    seval st0 = seval st1.
Proof.
  intros.
  induction H; simpl; auto; try rewrite IHstep; auto.
  apply step_pl_eq in H. rewrite H; auto.
Qed.

(** * Transitive Closures *)

Inductive lstar: St -> list Ev -> St -> Prop :=
| lstar_refl: forall st, lstar st [] st
| lstar_tran: forall st0 e st1 tr st2,
    step st0 (Some e) st1 -> lstar st1 tr st2 -> lstar st0 (e :: tr) st2
| lstar_silent_tran: forall st0 st1 tr st2,
    step st0 None st1 -> lstar st1 tr st2 -> lstar st0 tr st2.
#[export] Hint Resolve lstar_refl : core.

Lemma lstar_transitive:
  forall st0 tr0 st1 tr1 st2,
    lstar st0 tr0 st1 ->
    lstar st1 tr1 st2 ->
    lstar st0 (tr0 ++ tr1) st2.
Proof.
  intros.
  induction H.
  - rewrite app_nil_l; auto.
  - apply IHlstar in H0.
    rewrite <- app_comm_cons.
    eapply lstar_tran; eauto.
  - apply IHlstar in H0.
    eapply lstar_silent_tran; eauto.
Qed.

(** Transitive closure without labels. *)

Inductive star: St -> St -> Prop :=
| star_refl: forall st, star st st
| star_tran: forall st0 e st1 st2,
    step st0 e st1 -> star st1 st2 -> star st0 st2.
#[export] Hint Resolve star_refl : core.

Lemma star_transitive:
  forall st0 st1 st2,
    star st0 st1 ->
    star st1 st2 ->
    star st0 st2.
Proof.
  intros.
  induction H; auto.
  apply IHstar in H0.
  eapply star_tran; eauto.
Qed.

Lemma lstar_star:
  forall st0 tr st1,
    lstar st0 tr st1 -> star st0 st1.
Proof.
  intros.
  induction H; auto;
    eapply star_tran; eauto.
Qed.

Lemma star_lstar:
  forall st0 st1,
    star st0 st1 -> exists tr, lstar st0 tr st1.
Proof.
  intros.
  induction H; auto.
  - exists []; auto.
  - destruct IHstar as [tr G].
    destruct e.
    + exists (e :: tr).
      eapply lstar_tran; eauto.
    + exists tr.
      eapply lstar_silent_tran; eauto.
Qed.

Lemma star_seval:
  forall st0 st1,
    star st0 st1 -> seval st0 = seval st1.
Proof.
  intros.
  induction H; auto.
  apply step_seval in H; auto.
  rewrite H; auto.
Qed.

Lemma steps_preserves_eval:
  forall t p p' e0 e1,
    star (conf t p e0) (stop p' e1) ->
    aeval t p e0 = e1.
Proof.
  intros.
  apply star_seval in H.
  simpl in H; auto.
Qed.

(** * Correct Path Exists *)

Lemma star_strem:
  forall st0 st1 j p,
    star st0 st1 -> star (rem j p st0) (rem j p st1).
Proof.
  intros.
  induction H; auto.
  eapply star_tran; eauto.
Qed.

Lemma star_stls:
  forall st0 st1 t,
    star st0 st1 -> star (ls st0 t) (ls st1 t).
Proof.
  intros.
  induction H; auto.
  eapply star_tran; eauto.
Qed.

Lemma star_stbsl:
  forall st0 st1 j t p e,
    star st0 st1 ->
    star (bsl j st0 t p e) (bsl j st1 t p e).
Proof.
  intros.
  induction H; auto.
  eapply star_tran; eauto.
Qed.

Lemma star_stbsr:
  forall st0 st1 j e,
    star st0 st1 ->
    star (bsr j e st0) (bsr j e st1).
Proof.
  intros.
  induction H; auto.
  eapply star_tran; eauto.
Qed.

(* Congruence lemmas for Copland LTS semantics *)
Lemma lstar_stls :
  forall st0 st1 t tr,
    lstar st0 tr st1 -> lstar (ls st0 t) tr (ls st1 t).
Proof.
  intros.
  induction H; auto.
  eapply lstar_tran; eauto.
  eapply lstar_silent_tran; eauto.
Qed.

Lemma lstar_strem : forall st st' tr p r,
    lstar st tr
          st' ->
    lstar (rem r p st) tr (rem r p st').
Proof.
  intros.
  induction H; auto.
  eapply lstar_tran; eauto.
  eapply lstar_silent_tran; eauto.
Defined.

Lemma lstar_stbsl:
  forall st0 st1 j t p e tr,
    lstar st0 tr st1 ->
    lstar (bsl j st0 t p e) tr (bsl j st1 t p e).
Proof.
  intros.
  induction H; auto.
  eapply lstar_tran; eauto.
  eapply lstar_silent_tran; eauto.
Defined.

Lemma lstar_stbsr:
  forall st0 st1 j e tr,
    lstar st0 tr st1 ->
    lstar (bsr j e st0) tr (bsr j e st1).
Proof.
  intros.
  induction H; auto.
  eapply lstar_tran; eauto.
  eapply lstar_silent_tran; eauto.
Defined.

Lemma lstar_stbparl:
  forall st0 st1 st2 j tr,
    lstar st0 tr st1 ->
    lstar (bp j st0 st2) tr (bp j st1 st2).
Proof.
  intros.
  induction H; auto.
  eapply lstar_tran; eauto.
  eapply lstar_silent_tran; eauto.
Defined.

Lemma lstar_stbparr:
  forall st0 st1 st2 j tr,
    lstar st1 tr st2 ->
    lstar (bp j st0 st1) tr (bp j st0 st2).
Proof.
  intros.
  induction H; auto.
  eapply lstar_tran; eauto.
  eapply lstar_silent_tran; eauto.
Defined.

Lemma star_stbp:
  forall st0 st1 st2 st3 j,
    star st0 st1 ->
    star st2 st3 ->
    star (bp j st0 st2) (bp j st1 st3).
Proof.
  intros.
  induction H; auto.
  - induction H0; auto.
    eapply star_tran; eauto.
  - eapply star_tran; eauto.
Qed.

Theorem correct_path_exists:
  forall t p e,
    star (conf t p e) (stop p (aeval t p e)).
Proof.
  induction t; intros; simpl; eauto.
  - eapply star_tran; eauto.
  - (* destruct p. *)
    eapply star_tran; eauto.
    eapply star_transitive.
    apply star_strem.
    apply IHt.
    eapply star_tran; eauto.
  - eapply star_tran; eauto.
    eapply star_transitive.
    apply star_stls.
    apply IHt1.
    eapply star_tran; eauto.

  - eapply star_tran; eauto.
    eapply star_transitive.
    apply star_stbsl.
    apply IHt1.
    eapply star_tran; eauto.
    eapply star_transitive.
    apply star_stbsr.
    apply IHt2.
    eapply star_tran; eauto.

  -
    repeat dest_range.
    (*destruct p; destruct p0. *)
    eapply star_tran; eauto.
    eapply star_transitive.
    apply star_stbp.
    apply IHt1.
    apply IHt2.
    eapply star_tran; eauto.
Qed.

(** * Progress *)

Definition halt st :=
  match st with
  | stop _ _ => True
  | _ => False
  end.

(** The step relation nevers gets stuck. *)

Theorem never_stuck:
  forall st0,
    halt st0 \/ exists e st1, step st0 e st1.
Proof.
  induction st0.
  - left; simpl; auto.
  - right.
    destruct a.
    + exists (Some (asp_event (fst r) a p e)).
      eapply ex_intro; eauto.
    + exists (Some (req (fst r) p p0 (unanno a) e)).
      repeat dest_range.
      eapply ex_intro; eauto.
    + exists None.
      eapply ex_intro; eauto.

    + exists (Some (split (fst r) p)).
      eapply ex_intro; eauto.

    + exists (Some (Term_Defs.split(fst r) p)).
      (*destruct p; destruct p0. *)
      repeat dest_range.
      eapply ex_intro; eauto.
  -
    right.
    destruct IHst0.
    + destruct st0; simpl in H; try tauto.
      exists (Some (rpy (pred n) p p0 e)).
      eapply ex_intro; eauto.
    + destruct H as [e H].
      exists e.
      destruct H as [st1 H].
      exists (rem n p st1); auto.
  -
    right.
    destruct IHst0.
    + destruct st0; simpl in H; try tauto.
      exists None. eapply ex_intro; eauto.
    + destruct H as [e H].
      exists e.
      destruct H as [st H].
      exists (ls st a). auto.

  -
    right.
    destruct IHst0.
    + destruct st0; simpl in H; try tauto.
      exists None. eapply ex_intro; eauto.
    + destruct H as [e0 H].
      exists e0.
      destruct H as [st H].
      exists (bsl n st a p e). auto.
  - right.
    destruct IHst0.
    + destruct st0; simpl in H; try tauto.
      exists (Some (join (pred n) p)).
      eapply ex_intro; eauto.
    + destruct H as [e0 H].
      exists e0.
      destruct H as [st H].
      exists (bsr n e st). auto.

  - right.
    destruct IHst0_1 as [H|H].
    + destruct st0_1; simpl in H; try tauto.
      clear H.
      destruct IHst0_2.
      * destruct st0_2; simpl in H; try tauto.
        exists (Some (join (pred n) p0)).
        eapply ex_intro; eauto.
      * destruct H as [e0 H].
        exists e0.
        destruct H as [st H].
        exists (bp n (stop p e) st). auto.
    + destruct H as [e0 H].
      exists e0.
      destruct H as [st H].
      exists (bp n st st0_2). auto.
Qed.

(** * Termination *)

Inductive nstar: nat -> St -> St -> Prop :=
| nstar_refl: forall st, nstar 0 st st
| nstar_tran: forall st0 st1 st2 e n,
    nstar n st0 st1 -> step st1 e st2 -> nstar (S n) st0 st2.
#[export] Hint Resolve nstar_refl : core.

Lemma nstar_transitive:
  forall m n st0 st1 st2,
    nstar m st0 st1 ->
    nstar n st1 st2 ->
    nstar (m + n) st0 st2.
Proof.
  intros.
  induction H0.
  rewrite Nat.add_0_r; auto.
  apply IHnstar in H.
  eapply nstar_tran in H; eauto.
  rewrite plus_n_Sm in H.
  eauto.
Qed.

Lemma nstar_star:
  forall n st0 st1,
    nstar n st0 st1 -> star st0 st1.
Proof.
  intros.
  induction H; auto.
  eapply star_transitive; eauto.
  eapply star_tran; eauto.
Qed.

Lemma star_nstar:
  forall st0 st1,
    star st0 st1 ->
    exists n, nstar n st0 st1.
Proof.
  intros.
  induction H.
  - exists 0; auto.
  - destruct IHstar as [n G].
    exists (S n).
    rewrite <- Nat.add_1_l.
    eapply nstar_transitive; eauto.
    eapply nstar_tran; eauto.
Qed.

(** Size of a term (number of steps to reduce). *)

Fixpoint tsize t: nat :=
  match t with
  | aasp _ _ => 1
  | aatt _ _ x => 2 + tsize x
  | alseq _ x y => 2 + tsize x + tsize y
  | abseq _ _ x y => 3 + tsize x + tsize y
  | abpar _ _ x y => 2 + tsize x + tsize y
  end.

(** Size of a state (number of steps to reduce). *)

Fixpoint ssize s: nat :=
  match s with
  | stop _ _ => 0
  | conf t _ _ => tsize t
  | rem _ _ x => 1 + ssize x
  | ls x t => 1 + ssize x + tsize t
  | bsl _ x t _ _ => 2 + ssize x + tsize t
  | bsr _ _ x => 1 + ssize x
  | bp _ x y => 1 + ssize x + ssize y
  end.

(** Halt state has size 0. *)

Lemma halt_size:
  forall st,
    halt st <-> ssize st = 0.
Proof.
  split; intros.
  - destruct st; simpl in H; try tauto.
  - destruct st; simpl in H; try tauto;
      try discriminate.
    + simpl; auto.
    + destruct a; simpl in H; discriminate.
Qed.

(** A state decreases its size by one. *)

Lemma step_size:
  forall st0 e st1,
    step st0 e st1 ->
    S (ssize st1) = ssize st0.
Proof.
  intros.
  induction H; simpl; auto; lia.
Qed.

Lemma step_count:
  forall n t p e st,
    nstar n (conf t p e) st ->
    tsize t = n + ssize st.
Proof.
  induction n; intros.
  - inv H; simpl; auto.
  - inv H.
    apply IHn in H1.
    rewrite H1.
    apply step_size in H2.
    lia.
Qed.

(** Every run terminates. *)

Theorem steps_to_stop:
  forall t p e st,
    nstar (tsize t) (conf t p e) st ->
    halt st.
Proof.
  intros.
  apply step_count in H.
  apply halt_size.
  lia.
Qed.

(** * Numbered Labeled Transitions *)

Inductive nlstar: nat -> St -> list Ev -> St -> Prop :=
| nlstar_refl: forall st, nlstar 0 st [] st
| nlstar_tran: forall n st0 e st1 tr st2,
    step st0 (Some e) st1 -> nlstar n st1 tr st2 -> nlstar (S n) st0 (e :: tr) st2
| nlstar_silent_tran: forall n st0 st1 tr st2,
    step st0 None st1 -> nlstar n st1 tr st2 -> nlstar (S n) st0 tr st2.
#[export] Hint Resolve nlstar_refl : core.

Lemma nlstar_transitive:
  forall m n st0 tr0 st1 tr1 st2,
    nlstar m st0 tr0 st1 ->
    nlstar n st1 tr1 st2 ->
    nlstar (m + n) st0 (tr0 ++ tr1) st2.
Proof.
  intros.
  induction H.
  - rewrite app_nil_l; auto.
  - apply IHnlstar in H0.
    rewrite <- app_comm_cons.
    eapply nlstar_tran; eauto.
  - apply IHnlstar in H0.
    eapply nlstar_silent_tran; eauto.
Qed.

Lemma nlstar_lstar:
  forall n st0 tr st1,
    nlstar n st0 tr st1 -> lstar st0 tr st1.
Proof.
  intros.
  induction H; auto.
  - eapply lstar_tran; eauto.
  - eapply lstar_silent_tran; eauto.
Qed.

Lemma lstar_nlstar:
  forall st0 tr st1,
    lstar st0 tr st1 ->
    exists n, nlstar n st0 tr st1.
Proof.
  intros.
  induction H.
  - exists 0; auto.
  - destruct IHlstar as [n G].
    exists (S n).
    eapply nlstar_tran; eauto.
  - destruct IHlstar as [n G].
    exists (S n).
    eapply nlstar_silent_tran; eauto.
Qed.

Lemma nlstar_step_size:
  forall n st0 tr st1,
    nlstar n st0 tr st1 ->
    ssize st1 <= ssize st0.
Proof.
  intros.
  induction H; auto;
    apply step_size in H;
    lia.
Qed.

Lemma lstar_nlstar_size:
  forall st0 tr st1,
    lstar st0 tr st1 ->
    nlstar (ssize st0 - ssize st1) st0 tr st1.
Proof.
  intros.
  induction H.
  - rewrite Nat.sub_diag; auto.
  - pose proof H as G.
    apply step_size in G.
    rewrite <- G.
    rewrite <- minus_Sn_m.
    + eapply nlstar_tran; eauto.
    + apply nlstar_step_size in IHlstar; auto.
  - pose proof H as G.
    apply step_size in G.
    rewrite <- G.
    rewrite <- minus_Sn_m.
    + eapply nlstar_silent_tran; eauto.
    + apply nlstar_step_size in IHlstar; auto.
Qed.

(** The reverse version of [nlstar]. *)

Inductive rlstar: nat -> St -> list Ev -> St -> Prop :=
| rlstar_refl: forall st, rlstar 0 st [] st
| rlstar_tran: forall n st0 e st1 tr st2,
    rlstar n st0 tr st1 -> step st1 (Some e) st2 ->
    rlstar (S n) st0 (tr ++ [e]) st2
| rlstar_silent_tran: forall n st0 st1 tr st2,
    rlstar n st0 tr st1 -> step st1 None st2 ->
    rlstar (S n) st0 tr st2.
#[export] Hint Resolve rlstar_refl : core.

Lemma rlstar_transitive:
  forall m n st0 tr0 st1 tr1 st2,
    rlstar m st0 tr0 st1 ->
    rlstar n st1 tr1 st2 ->
    rlstar (m + n) st0 (tr0 ++ tr1) st2.
Proof.
  intros.
  induction H0.
  - rewrite Nat.add_0_r; rewrite app_nil_r; simpl; auto.
  - apply IHrlstar in H.
    rewrite Nat.add_succ_r.
    rewrite app_assoc.
    eapply rlstar_tran; eauto.
  - apply IHrlstar in H.
    rewrite Nat.add_succ_r.
    eapply rlstar_silent_tran; eauto.
Qed.

Lemma rlstar_lstar:
  forall n st0 tr st1,
    rlstar n st0 tr st1 -> lstar st0 tr st1.
Proof.
  intros.
  induction H; auto.
  - eapply lstar_transitive; eauto.
    eapply lstar_tran; eauto.
  - rewrite <- app_nil_r with (l:=tr).
    eapply lstar_transitive; eauto.
    apply lstar_silent_tran with st2; auto.
Qed.

Lemma lstar_rlstar:
  forall st0 tr st1,
    lstar st0 tr st1 ->
    exists n, rlstar n st0 tr st1.
Proof.
  intros.
  induction H.
  - exists 0; auto.
  - destruct IHlstar as [n G].
    exists (S n).
    cut (rlstar (1 + n) st0 ([e] ++ tr) st2).
    simpl; auto.
    eapply rlstar_transitive; eauto.
    cut (rlstar 1 st0 ([] ++ [e]) st1).
    simpl; auto.
    eapply rlstar_tran; eauto.
  - destruct IHlstar as [n G].
    exists (S n).
    cut (rlstar (1 + n) st0 ([] ++ tr) st2).
    rewrite app_nil_l; auto.
    eapply rlstar_transitive; eauto.
    eapply rlstar_silent_tran; eauto.
Qed.

Lemma rlstar_nlstar:
  forall n st0 tr st1,
    rlstar n st0 tr st1 <-> nlstar n st0 tr st1.
Proof.
  split; intros.
  - induction H; auto.
    + rewrite <- Nat.add_1_r.
      eapply nlstar_transitive; eauto.
      eapply nlstar_tran; eauto.
    + rewrite <- Nat.add_1_r.
      rewrite <- app_nil_r with (l:=tr).
      eapply nlstar_transitive; eauto.
      eapply nlstar_silent_tran; eauto.
  - induction H; auto.
    + rewrite <- Nat.add_1_l.
      assert (G: e :: tr = [e] ++ tr).
      simpl; auto.
      rewrite G.
      eapply rlstar_transitive; eauto.
      rewrite <- app_nil_l with (l:=[e]).
      eapply rlstar_tran; eauto.
    + rewrite <- Nat.add_1_l.
      rewrite <- app_nil_l with (l:=tr).
      eapply rlstar_transitive; eauto.
      eapply rlstar_silent_tran in H; eauto.
Qed.

author: ku-sldg

repo: copland-avm

save_path: github-repos/coq/ku-sldg-copland-avm


text:
Require Import core.Semantics.
Require Import core.modeling.ModelingSemantics.
Require Import core.modeling.ConcreteSyntax.
Require Import core.modeling.Parser.
Require Import core.Model.
Require Import core.TransformationConfiguration.
Require Import core.modeling.ModelingTransformationConfiguration.
Require Import String.
Require Import EqNat.
Require Import List.
Require Import Expressions.
Require Import core.utils.Utils.
Require Import PeanoNat.
Require Import Lia.

(*************************************************************)
(** * Additivity in OutputPatternElement context             *)
(*************************************************************)

Definition Rule_incl_modeling_elements {tc: TransformationConfiguration} {mtc: ModelingTransformationConfiguration tc}
  (x y: ConcreteRule) : Prop :=
  ConcreteRule_getName x = ConcreteRule_getName y
  /\ ConcreteRule_getInTypes x = ConcreteRule_getInTypes y
  /\ ConcreteRule_getGuard x = ConcreteRule_getGuard y
  /\ ConcreteRule_getIteratedList x = ConcreteRule_getIteratedList y
  /\ subseq (ConcreteRule_getConcreteOutputPattern x) (ConcreteRule_getConcreteOutputPattern y).

Inductive Transformation_incl_modeling_rules {tc: TransformationConfiguration}  : list Rule -> list Rule -> Prop :=
  | incl_rules_nil : Transformation_incl_modeling_rules nil nil
  | incl_rules_diff : forall x y xs ys, Transformation_incl_modeling_rules xs ys
    -> Rule_incl_modeling_elements x y
    -> Transformation_incl_modeling_rules (x::xs) (y::ys).

Definition Transformation_incl_modeling_elements {tc: TransformationConfiguration} (t1 t2: Transformation) : Prop :=
  (Transformation_getArity t1 = Transformation_getArity t2) /\
  Transformation_incl_rules' (Transformation_getRules t1) (Transformation_getRules t2).

Theorem additivity_modeling_elements :
forall (tc: TransformationConfiguration) (t1 t2: Transformation) (sm: SourceModel),
  (Transformation_incl_elements'' t1 t2 ->
    incl (allModelElements (execute t1 sm)) (allModelElements (execute t2 sm))).
Proof.
Admitted.

author: atlanmod

repo: coqtl

save_path: github-repos/coq/atlanmod-coqtl


text:
(*
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 * http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 *)

Require Import CompilerRuntime.
Require String.
Require QData.
Require QOperators.
Require LambdaNRA.
Require LambdaNRASugar.

Module QLambdaNRA(runtime:CompilerRuntime).

  Module Data := QData.QData runtime.
  Module Ops := QOperators.QOperators runtime.

  Definition expr : Set
    := LambdaNRA.lambda_nra.
  Definition lambda_expr : Set
    := LambdaNRA.lnra_lambda.
  Definition t : Set
    := expr.
  Definition var : Set
    := String.string.

  Definition lalambda : var -> expr -> lambda_expr
    := LambdaNRA.LNRALambda.
  Definition lavar : var -> expr
    := LambdaNRA.LNRAVar.
  Definition laconst : Data.qdata -> expr
    := LambdaNRA.LNRAConst.
  Definition latable  : String.string -> expr
    := LambdaNRA.LNRATable.
  Definition labinop : Ops.Binary.op -> expr -> expr -> expr
    := LambdaNRA.LNRABinop.
  Definition launop : Ops.Unary.op -> expr -> expr
    := LambdaNRA.LNRAUnop.
  Definition lamap : lambda_expr -> expr -> expr
    := LambdaNRA.LNRAMap.
  Definition lafilter : lambda_expr -> expr -> expr
    := LambdaNRA.LNRAFilter.
  Definition lamapproduct : lambda_expr -> expr -> expr
    := LambdaNRA.LNRAMapProduct.
  Definition laproduct : expr -> expr -> expr
    := LambdaNRA.LNRAProduct.

  Definition ladot : String.string -> expr -> expr
    := LambdaNRASugar.LNRADot.
  Definition laarrow : String.string -> expr -> expr
    := LambdaNRASugar.LNRAArrow.
  Definition lastruct : list (String.string * expr) -> expr
    := LambdaNRASugar.LNRAStruct.
  Definition laflatmap : lambda_expr -> expr -> expr
    := LambdaNRASugar.LNRAFlatMap.

  Definition latableify : expr -> expr
    := LambdaNRASugar.la_tableify.

End QLambdaNRA.

author: querycert

repo: qcert

save_path: github-repos/coq/querycert-qcert