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.
 *)

(** This module provides support for bindings where the key is a
natural number. *)

Require Import Arith.
Require Import NPeano.
Require Import Bindings.

Section BindingsNat.

  Global Program Instance ODT_nat : (@ODT nat)
    := mkODT _ _ lt Nat.lt_strorder lt_dec Nat.compare _.
  Next Obligation.
    simpl.
    apply Nat.compare_spec.
  Qed.

End BindingsNat.

Global Hint Unfold rec_sort rec_concat_sort : qcert.
Global Hint Resolve drec_sort_sorted drec_concat_sort_sorted : qcert.
Global Hint Resolve is_list_sorted_NoDup_strlt : qcert.

author: querycert

repo: qcert

save_path: github-repos/coq/querycert-qcert


text:
Require Export cpt3structureddata.

(* Polymorphism *)
(* Polymorphic lists *)

(* new inductive datatype? we can do polymorphic inductive type defs! *)
Inductive list (X:Type) : Type :=
| nil : list X
| cons : X -> list X -> list X.

(* Exactly like the def. of natlist but nat arg is replaced with arbitary X *)

Check nil.
Check cons.

(* Now we can make polymorphic or "generic" versions of all list funcs! *)

Fixpoint length (X:Type) (l:list X) : nat :=
  match l with
    | nil _ => 0 (* underscore added since arg is noninformative *)
    | cons _ h t => S (length X t) (* some update in coq version i think *)
  end.

Example test_length1 :
    length nat (cons nat 1 (cons nat 2 (nil nat))) = 2.
Proof. reflexivity. Qed.
Example test_length2 :
    length bool (cons bool true (nil bool)) = 1.
Proof. reflexivity. Qed.

Fixpoint app (X : Type) (l1 l2 : list X)
                : (list X) :=
  match l1 with
  | nil _ => l2
  | cons _ h t => cons X h (app X t l2)
  end.

Fixpoint snoc (X:Type) (l:list X) (v:X) : (list X) :=
  match l with
  | nil _ => cons X v (nil X)
  | cons _ h t => cons X h (snoc X t v)
  end.

Fixpoint rev (X:Type) (l:list X) : list X :=
  match l with
  | nil _ => nil X
  | cons _ h t => snoc X (rev X t) h
  end.

Example test_rev1 :
    rev nat (cons nat 1 (cons nat 2 (nil nat)))
  = (cons nat 2 (cons nat 1 (nil nat))).
Proof. reflexivity. Qed.

Example test_rev2:
  rev bool (nil bool) = nil bool.
Proof. reflexivity. Qed.

Module MumbleBaz.

  Inductive mumble : Type :=
  | a : mumble
  | b : mumble -> nat -> mumble
  | c : mumble.
  Inductive grumble (X:Type) : Type :=
  | d : mumble -> grumble X
  | e : X -> grumble X.

  (* Exercise 2 baz_num_elts *)

  Inductive baz : Type :=
  | x : baz -> baz
  | y : baz -> bool -> baz.

End MumbleBaz.

(* Type annotation inference *)

Fixpoint app' X l1 l2 : list X :=
  match l1 with
  | nil _      => l2
  | cons _ h t => cons X h (app' X t l2)
  end.

(* What type did Coq assign to app'? *)
Check app'.
Check app.

(* Type argument synthesis *)

Fixpoint length' (X:Type) (l:list X) : nat :=
  match l with
    | nil _ => 0
    | cons _ h t => S (length' _ t)
  end.
(* length using implicit args *)

(* Implicit args *)

Arguments nil {X}.
Arguments cons {X} _ _.
Arguments length {X} l.
Arguments app {X} l1 l2.
Arguments rev {X} l.
Arguments snoc {X} l v.

Definition list123'' := cons 1 (cons 2 (cons 3 nil)).
Check (length list123'').

(* OR we could declare an arg to be implicit while defininging the func
itself, by surrounding the arg in curly braces *)
Fixpoint length'' {X:Type} (l:list X) : nat :=
  match l with
    | nil => 0
    | cons h t => S (length'' t)
  end.

(* Sometimes coq doesn't have enough local info to determine type argument
so we define something *)

(* Polymorphic lists exercises *)
Fixpoint repeat {X:Type} (n:X) (count:nat) : list X :=
  match count with
    | 0 => nil
    | S m => n :: repeat n m
  end.

Example test_repeat1:
  repeat true 2 = cons true (cons true nil).
Proof. simpl. reflexivity. Qed.

Theorem nil_app : forall X:Type, forall l:list X,
                    app [] l = l.
Proof.
  simpl. reflexivity.
Qed.

Theorem rev_snoc : forall X : Type,
                   forall v : X,
                   forall s : list X,
                     rev (snoc s v) = v :: (rev s).
Proof.
  intros.
  induction s.
  simpl. reflexivity.
  simpl. rewrite -> IHs. simpl. reflexivity.
Qed.

author: soojison

repo: Software-Foundations


text:
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Import BinPos.
Require Export List.
Set Implicit Arguments.
Local Open Scope positive_scope.

Section MakeBinList.
 Variable A : Type.
 Variable default : A.

 Fixpoint jump (p:positive) (l:list A) {struct p} : list A :=
  match p with
  | xH => tl l
  | xO p => jump p (jump p l)
  | xI p  => jump p (jump p (tl l))
  end.

 Fixpoint nth (p:positive) (l:list A) {struct p} : A:=
  match p with
  | xH => hd default l
  | xO p => nth p (jump p l)
  | xI p => nth p (jump p (tl l))
  end.

 Lemma jump_tl : forall j l, tl (jump j l) = jump j (tl l).
 Proof.
  induction j;simpl;intros; now rewrite ?IHj.
 Qed.

 Lemma jump_succ : forall j l,
  jump (Pos.succ j) l = jump 1 (jump j l).
 Proof.
  induction j;simpl;intros.
  - rewrite !IHj; simpl; now rewrite !jump_tl.
  - now rewrite !jump_tl.
  - trivial.
 Qed.

 Lemma jump_add : forall i j l,
  jump (i + j) l = jump i (jump j l).
 Proof.
  induction i using Pos.peano_ind; intros.
  - now rewrite Pos.add_1_l, jump_succ.
  - now rewrite Pos.add_succ_l, !jump_succ, IHi.
 Qed.

 Lemma jump_pred_double : forall i l,
  jump (Pos.pred_double i) (tl l) = jump i (jump i l).
 Proof.
  induction i;intros;simpl.
  - now rewrite !jump_tl.
  - now rewrite IHi, <- 2 jump_tl, IHi.
  - trivial.
 Qed.

 Lemma nth_jump : forall p l, nth p (tl l) = hd default (jump p l).
 Proof.
  induction p;simpl;intros.
  - now rewrite <-jump_tl, IHp.
  - now rewrite <-jump_tl, IHp.
  - trivial.
 Qed.

 Lemma nth_pred_double :
  forall p l, nth (Pos.pred_double p) (tl l) = nth p (jump p l).
 Proof.
  induction p;simpl;intros.
  - now rewrite !jump_tl.
  - now rewrite jump_pred_double, <- !jump_tl, IHp.
  - trivial.
 Qed.

End MakeBinList.

author: Priyanka-Mondal

repo: Coq

save_path: github-repos/coq/Priyanka-Mondal-Coq


text:
(*

  Copyright 2016 University of Luxembourg

  This file is part of our formalization of Platzer's
    "A Complete Uniform Substitution Calculus for Differential Dynamic Logic"
  available here: http://arxiv.org/pdf/1601.06183.pdf (July 27, 2016).
  We refer to this formalization as DdlCoq here.

  DdlCoq is free software: you can redistribute it and/or modify
  it under the terms of the GNU General Public License as published by
  the Free Software Foundation, either version 3 of the License, or
  (at your option) any later version.

  DdlCoq is distributed in the hope that it will be useful,
  but WITHOUT ANY WARRANTY; without even the implied warranty of
  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  GNU General Public License for more details.

  You should have received a copy of the GNU General Public License
  along with DdlCoq.  If not, see <http://www.gnu.org/licenses/>.

  authors:
    Vincent Rahli
    Marcus Völp
    Ivana Vukotic

 *)

Require Export static_sem_lemmas.

(** Bound effect --- see Lemma 1, Section 2.4 *)
Lemma bound_effect_lemma :
  forall alpha I v w,
    dynamic_semantics_program I alpha v w
    -> equal_states_on_complement v w (bound_vars_program alpha).
Proof.
  unfold equal_states_on_complement;
    prog_ind alpha Case; simpl; introv ds i;
      ginv; try (complete (inversion i)).

  { Case "KPassign".
    repeat (dest_cases x; GC).
    eapply differ_state_except_prop1; eauto.
  }

  { Case "KPassignAny".
    introv h.
    repeat (dest_cases x; GC).
    exrepnd.
    eapply differ_state_except_prop1; eauto. }

  { Case "KPtest".
    repnd; subst; auto.
  }

  { Case "KPchoice".
    apply in_eassignables_app_false_implies in i; repnd.
    repndors;[|].
    - apply (IHalpha1 I); auto.
    - apply (IHalpha2 I); auto.
  }

  { Case "KPcompose".
    apply in_eassignables_app_false_implies in i; repnd.
    exrepnd.
    pose proof (IHalpha1 I v s ds1 a i0) as h1.
    pose proof (IHalpha2 I s w ds0 a i) as h2.
    congruence.
  }

  { Case "KPloop".
    induction ds; auto.
    rewrite IHds; clear IHds.
    apply (IHalpha I); auto.
  }

  { Case "KPodeSystem".
    pose proof (equal_states_upto_prop1 a v w (ode_footprint I ode)) as q.
    repeat (autodimp q hyp);
      [|intro j;
        apply in_ode_footprint_implies_in_bound_vars in j;
        rewrite i in j; ginv];[].

    exrepnd; subst.
    pose proof (ds1 (mk_preal_upto r r (Rle_refl r))) as h; clear ds1; simpl in h; repnd.
    introv j.
    rewrite <- h; auto.
    apply ds0; intro xx.
    apply ode_footprint_diff_subset_ode_footprint in xx; auto. }
Qed.

author: LS-Lab

repo: Coq-dL

save_path: github-repos/coq/LS-Lab-Coq-dL


text:
Require Import chap13.

Set Implicit Arguments.

CoFixpoint LMap (A B: Type)(f : A -> B) (u : LList A) : LList B :=
  match u with
   LNil => (LNil (A:=B))
  |LCons x u' => LCons (f x) (LMap  f u')
  end.

(* example *)

Definition cubes := LMap (fun x => x * x * x) (from 0).

(** Tests :
Eval simpl in (LList_decomp_n 5 cubes).

*)

(*

CoFixpoint LMapcan (A B: Set) (f : A -> LList B)(u : LList A) : LList B :=
   match u with
   LNil => (LNil (A:=B))
  |LCons x u' => LAppend (f x) (LMapcan  f u')
  end.

Recursive definition of LMapcan is ill-formed.
In environment
LMapcan : forall A B : Set, (A -> LList B) -> LList A -> LList B
A : Set
B : Set
f : A -> LList B
u : LList A
x : A
u' : LList A
unguarded recursive call in
(cofix LAppend (A : Set) (u v : LList A) : LList A :=
   match u with
   | LNil => v
   | LCons a u' => LCons a (LAppend A u' v)
   end)

Notice that, if such a LMapcan would be defineable, the evaluation of
the following term would loop ! :

LHead (LMapcan (fun n => match (Peano_dec.eq_nat_dec n (n+1))
                with left _ => (LCons 1 LNil)
                   | right _ => LNil (A:= nat)
                end)
               (from 0))

*)

author: raduom

repo: coq-art

save_path: github-repos/coq/raduom-coq-art


text:
(* Permet d'éliminer les paramètres par défaut dans les définitions sur des types polymorphes.
   Par exemple si un élement n'est pas dans une liste de region on pourra renvoyer None plutot qu'une valeur par défaut comme Z.
   Voir [natoption] pour plus d'infos. *)
Inductive option {A:Type}: Type :=
  | Some : A -> option
  | None : option.

(* Permet d'additioner des option de type nat sans passer par des fonctions auxiliaires. *)
Definition add_opt (a b:@option nat):@option nat :=
match a, b with
| Some a', Some b' => Some (a'+b')
| _, _ => None
end.
(* Permet d'extraire l'élement d'un type [option] et de renvoyer
   une valeur par défaut fournie en argument dans le cas [None]. *)
Definition option_elim {A:Type} (d: A) (o: option): A :=
  match o with
  | Some n' => n'
  | None => d
  end.

author: ArthurWenger

save_path: github-repos/coq/ArthurWenger-Coq


text:
Require Import String.
Open Scope string_scope.
Require Import Coq.Lists.List.
Import ListNotations.

Require Import Parser.
Require Import parser.

Definition str_map (X : Type) := list (prod string X).
Fixpoint str_map_get (X : Type) (m : str_map X) (k : string) (def : X) : X :=
match m with
| cons h t => if string_dec (fst h) k then snd h else str_map_get X t k def
| nil => def
end.

Inductive uexpr_type : Set :=
| t_string
| t_boolean
| t_list
| t_void
| t_fn
| t_error.

Inductive uexpr_val : Set :=
| v_string : string -> uexpr_val
| v_boolean : bool -> uexpr_val
| v_list : list uexpr_val -> uexpr_val
| v_void : uexpr_val
| v_fn : uexpr -> uexpr_val
| v_error : uexpr_val.

Definition uexpr_env := str_map uexpr_val.

Inductive uexpr_eval : uexpr_env -> uexpr -> uexpr_env -> uexpr_val -> Prop :=
| eval_string
  (n : uexpr_env)
  (s : string)
  : uexpr_eval n (e_string s) n (v_string s)
| eval_block_empty
  (n : uexpr_env)
  : uexpr_eval n (e_block nil) n (v_void)
| eval_block_single
  (n_1 n_2 : uexpr_env)
  (e : uexpr)
  (v : uexpr_val)
  (H : uexpr_eval n_1 e n_2 v)
  : uexpr_eval n_1 (e_block (cons e nil)) n_2 v
| eval_block_cons
  (n_head_1 n_head_2 n_tail_2 : uexpr_env)
  (e_head e_tail_h : uexpr)
  (e_tail_t : list uexpr)
  (v_head v_tail : uexpr_val)
  (H_head : uexpr_eval n_head_1 e_head n_head_2 v_head)
  (H_tail : uexpr_eval n_head_2 (e_block (e_tail_h :: e_tail_t)) n_tail_2 v_tail)
  : uexpr_eval n_head_1 (e_block (e_head :: e_tail_h :: e_tail_t)) n_tail_2 v_tail
| eval_call
  (n_1 n_2 : uexpr_env)
  (var : string)
  (e : uexpr)
  (v : uexpr_val)
  (H_eval : uexpr_eval n_1 e n_2 v)
  (H_get : str_map_get _ n_1 var v_error = v_fn e)
   : uexpr_eval n_1 (e_call var []) n_2 v
| eval_var
  (var : string)
  (n : uexpr_env)
  : uexpr_eval n (e_var var) n (str_map_get _ n var v_error)
| eval_neg
  (n1 n2 : uexpr_env)
  (v : uexpr_val)
  (e : uexpr)
  (H : uexpr_eval n1 e n2 v)
  : uexpr_eval n1 (e_unop unop_neg e) n2 (
    match v with
    | v_boolean b => v_boolean (negb b)
    | _ => v_error
    end)
| eval_eq_on_strings
  (n1 n2 n3 : uexpr_env)
  (s1 s2 : string)
  (e1 e2 : uexpr)
  (H1 : uexpr_eval n1 e1 n2 (v_string s1))
  (H2 : uexpr_eval n2 e2 n3 (v_string s2))
  : uexpr_eval n1 (e_binop binop_eq e1 e2) n3 (v_boolean (if string_dec s1 s2 then true else false))
| eval_let
  (n1 n2 : uexpr_env)
  (var : string)
  (e : uexpr)
  (v : uexpr_val)
  (H : uexpr_eval n1 e n2 v)
  : uexpr_eval n1 (e_call "let" [e_var var; e]) ((var, v) :: n2) (v_void)
| eval_let_fn
  (n : uexpr_env)
  (var : string)
  (e : uexpr)
   : uexpr_eval n (e_call "let_fn" [e_var var; e]) ((var, v_fn e) :: n) (v_void)
.

Definition my_eval : forall
  (fuel : nat)
  (n1 : uexpr_env)
  (e : uexpr),
  option { n2 : uexpr_env & { v : uexpr_val & uexpr_eval n1 e n2 v } }.
Proof.
  refine (fix my_eval (fuel : nat) (n1 : uexpr_env) (e : uexpr)
  : option { n2 : uexpr_env & { v : uexpr_val & uexpr_eval n1 e n2 v } } :=
match fuel with
| S f =>
match e with
| e_string s => Some (existT _ n1 (existT _ (v_string s) (eval_string n1 s)))
| e_block nil => Some (existT _ n1 (existT _ (v_void) (eval_block_empty n1)))
| e_block (e1 :: nil) =>
    match my_eval f n1 e1 with
    | Some (existT _ n2 (existT _ v pf)) =>
        Some (existT _ n2 (existT _ v (eval_block_single n1 n2 e1 v pf)))
    | _ => None
    end
| e_block (e_head :: e_tail_h :: e_tail_t) =>
    match my_eval f n1 e_head with
    | Some (existT _ n_head_2 (existT _ v_head H_head)) =>
        match my_eval f n_head_2 (e_block (e_tail_h :: e_tail_t)) with
        | Some (existT _ n_tail_2 (existT _ v_tail H_tail)) =>
            Some (existT _ n_tail_2 (existT _ v_tail (
              eval_block_cons n1 n_head_2 n_tail_2 e_head e_tail_h e_tail_t v_head v_tail H_head H_tail
            )))
        | _ => None
        end
    | _ => None
    end
| e_var var =>
    Some (existT _ n1 (existT _ (str_map_get _ n1 var v_error) (
      eval_var var n1
    )))
| e_unop unop_neg e1 =>
    match my_eval f n1 e1 with
    | Some (existT _ n2 (existT _ v pf)) =>
      Some (existT _ n2 (existT _ (
    match v with
    | v_boolean b => v_boolean (negb b)
    | _ => v_error
    end) (eval_neg n1 n2 v e1 pf)))
    | _ => None
  end
| e_binop binop_eq e1 e2 => match my_eval f n1 e1 with
    | Some (existT _ n2 (existT _ (v_string s1) pf1)) => match my_eval f n2 e2 with
      | Some (existT _ n3 (existT _ (v_string s2) pf2)) =>
        Some (existT _ n3 (existT _ (v_boolean (if string_dec s1 s2 then true else false))
          (eval_eq_on_strings n1 n2 n3 s1 s2 e1 e2 pf1 pf2)))
      | _ => None
    end
    | _ => None
  end
| e_call "let" [e_var var; e1] =>
    match my_eval f n1 e1 with
    | Some (existT _ n2 (existT _ v H)) =>
        Some (existT _ ((var, v) :: n2) (existT _ v_void (
          eval_let n1 n2 var e1 v H
        )))
    | _ => None
    end
| e_call "let_fn" [e_var var; e1] =>
    Some (existT _ ((var, v_fn e1) :: n1) (existT _ v_void (
      eval_let_fn n1 var e1
    )))
| e_call var [] =>
    let get_res := str_map_get _ n1 var v_error in
    let H_get : str_map_get _ n1 var v_error = get_res := eq_refl get_res in
    (match get_res with
    | v_fn e =>
        fun H_get => match my_eval f n1 e with
        | Some (existT _ n_2 (existT _ v H_eval)) =>
            Some (existT _ n_2 (existT _ v (
            eval_call n1 n_2 var e v H_eval H_get
            )))
        | _ => None
        end
    | _ => fun _ => None
   end H_get)
| _ => None
end
| O => None
end).
Defined.

Definition eval_e (fuel : nat) (e : uexpr) :=
  match my_eval fuel nil e with
  | Some (existT _ n (existT _ v pf)) => Some (n, v)
  | _ => None
  end
.

Theorem eval_e_correct :
  forall
    (e : uexpr)
    (fuel : nat)
    (n : uexpr_env)
    (v : uexpr_val),
    eval_e fuel e = Some (n, v) -> uexpr_eval nil e n v
.
Proof.
  intros.
  unfold eval_e in H.
  destruct (my_eval fuel nil e).
  - destruct s. destruct s. injection H as H. rewrite <- H. rewrite <- H0. assumption.
  - discriminate H.
Qed.

Definition eval (fuel : nat) (s : string) :=
  match parse s with
  | Res e => eval_e fuel e
  | Err _ => None
  end
.

Definition eval_good (v_exp : uexpr_val) (e: string) :=
  match eval 100 e with
  | Some (n, v) => v = v_exp
  | _ => False
  end.

Goal eval_good (v_string "a") "a". cbv. reflexivity. Qed.
Goal eval_good (v_error) "~a". cbv. reflexivity. Qed.
Goal eval_good (v_boolean false) "~(a=a)". cbv. reflexivity. Qed.

Compute (eval 100 "
{
  let($b, a=a);
  let_fn($flip, let($b, ~$b));
  let_fn($rec, rec());
  flip();
  flip();
  flip();
  flip();
  $b;
}
").

author: kuruczgy


text:
(* -----------------------------------------------------------
   UNIVERSIDADE FEDERAL DO CEARÁ - DEPARTAMENTO DE COMPUTAÇÃO

   AVALIAÇÃO PARCIAL 2, NO SEMESTRE LETIVO 2016.2, DAS TURMAS:

     - CK0230 - PROVA ASSISTIDA POR COMPUTADOR - T01
     - CK0130 - TEORIA DA PROVA                - T01 .

   PROFESSOR: PABLO MAYCKON SILVA FARIAS.
   ----------------------------------------------------------- *)

(*
   DADOS DO ALUNO: MATRÍCULA: Marcos Felipe de Menezes Mota
                   NOME     : 354080
*)

(*
   INTRODUÇÃO: Caro aluno, esta prova possui 2 questões:

      - Q1: 4 pontos.
      - Q2: 1 ponto.

   Você deve escrever neste arquivo as respostas dessas questões, e
   então enviá-lo de volta para mim por e-mail, dentro do tempo de
   realização da prova.

   Por favor, coopere com o processo de ensino e aprendizagem desta
   disciplina e não compartilhe este arquivo com outras pessoas, nem
   durante nem depois da realização da prova. Obrigado!

   ATENÇÃO: AS ÚNICAS FONTES PERMITIDAS PARA CONSULTA são os
            capítulos que estudamos do livro da disciplina, além do
   manual do coq, para esclarecimentos sobre os recursos que foram
   estudados.

   IMPORTANTE: Ao responder às questões, você pode e deve usar
               definições e teoremas dos capítulos já estudados:
   a função do comando a seguir é justamente importar esses recursos.
*)

Require Export Logic.

(* =============================== QUESTÃO  1 =============================== *)

Module Q1. (* 4 PONTOS *)

(*
   RESUMO: nesta questão você deve:

     A) Definir um tipo "Deque".
     B) Escrever funções para remover do início e do fim de Deques,
        assim como para calcular o tamanho de uma Deque.
     C) Provar um teorema sobre tamanhos de Deques após remoções.

   Mais informações seguem abaixo.
*)

(* PARTE 1: Defina um tipo Deque, que armazene números naturais e
            permita inserções e remoções no início e no fim da
   estrutura -- mas não escreva nenhuma função ainda!

   ATENÇÃO: Você poderia fornecer uma definição indutiva para esse
   tipo, mas é mais rápido defini-lo em termos do tipo "list", para o
   qual já temos vários recursos à disposição!

   Não é necessário definir notações para esse tipo e nem para as
   funções abaixo.
*)

Definition Deque := list nat.

(* PARTE 2: Defina 3 funções: a primeira para remover do início e a
            segunda para remover do fim da Deque recebida como
   argumento. Essas duas primeiras funções devem retornar UM PAR
   ORDENADO, contendo:

     - Um "option nat", contendo o elemento removido (ou nada, caso a
       deque esteja vazia).

     - A deque resultante da remoção (que será a mesma dada como
       entrada quando esta estiver vazia).

   A terceira função deve retornar o número de elementos da Deque.
*)

SearchAbout list.

Definition remove_head (d : Deque) : option nat * Deque :=
  match d with
  | [] => (None, d)
  | h :: t => (Some h, t)
  end.

Fixpoint remove_tail (d : Deque) : option nat * Deque :=
  match d with
  | nil => (None, d)
  | h :: t => match t with
              | nil => (Some h, t)
              | h1 :: t1 => (fst(remove_tail t), h :: snd (remove_tail t))
              end
  end.

Compute(remove_tail [2;3;4;5]).

(* PARTE 3: Prove que, para toda deque "d", se de "d" é removido o
            elemento do início, em seguida é removido o elemento do
   final, e se esta segunda remoção de fato retorna um número, então
   o tamanho de "d" é 2 unidades a mais que o tamanho da deque após a
   segunda remoção.

   DICA: escreva um lema relacionando a forma de uma deque antes e
         depois de uma remoção do final da estrutura.
*)

Lemma length_remove_tail: forall (d : Deque), length(snd(remove_tail d)) + 1 = length d.
Proof.
  induction d.
  - simpl. symmetry. admit.
  - admit.
Qed.

Lemma plus_Sn_1: forall n: nat, S n = n+1.
Proof.
  induction n.
  - reflexivity.
  - simpl. rewrite IHn. reflexivity.
Qed.

Theorem part3 : forall (d : Deque) (n:nat),
        length(snd(remove_tail(snd(remove_head d)))) + 2 = (length d) ->
        fst (remove_tail(snd(remove_head d))) = Some n.
Proof.
  intros. induction d as [|h t IHd].
  - simpl. simpl in H. inversion H.
  - simpl. simpl in H.
    admit.
Qed.

End Q1.

(* =============================== QUESTÃO  2 =============================== *)

Module Q2. (* 1 PONTO *)

(* PROVE ESTE TEOREMA: *)

Theorem em_demorgan: excluded_middle -> de_morgan_not_and_not.
  unfold de_morgan_not_and_not. unfold excluded_middle.
  unfold not. intros. destruct H0. split.
  - intros. apply double_neg in H0.

End Q2.

(* ================================== FIM  ================================== *)

author: marcosfmmota

repo: software-foundations


text:
Require Import HoareDef MutHeader MutG0 MutG1 SimModSem.
Require Import Coqlib.
Require Import ImpPrelude.
Require Import Skeleton.
Require Import PCM.
Require Import ModSem Behavior.
Require Import Relation_Definitions.

(*** TODO: export these in Coqlib or Universe ***)
Require Import Relation_Operators.
Require Import RelationPairs.
From ITree Require Import
     Events.MapDefault.
From ExtLib Require Import
     Core.RelDec
     Structures.Maps
     Data.Map.FMapAList.

Require Import HTactics ProofMode.

Set Implicit Arguments.

Local Open Scope nat_scope.

Section SIMMODSEM.

  Context `{Σ: GRA.t}.

  Let W: Type := Any.t * Any.t.

  Let wf: _ -> W -> Prop :=
    mk_wf (fun (_: unit) _ _ => (True: iProp)%I).

  Theorem correct: refines2 [MutG0.G] [MutG1.G].
  Proof.
    eapply adequacy_local2. econs; ss.
    i. econstructor 1 with (wf:=wf) (le:=top2); et.
    { ss. }
    2: { exists tt. econs; ss; rr; uipropall. }
    econs; ss. init. harg. mDesAll.
    des; clarify. unfold gF, ccallU. steps. astart 10.
    force_r.
    { eapply mut_max_intrange. auto. } steps.
    destruct (dec (Z.of_nat x) 0%Z).
    - destruct x; ss. astop. steps. force_l. eexists. steps.
      hret _; ss.
    - destruct x; [ss|]. rewrite Nat2Z.inj_succ. steps.
      acatch. hcall _ _ with "*"; auto.
      { iPureIntro.
        replace (Z.succ (Z.of_nat x) - 1)%Z with (Z.of_nat x) by lia.
        esplits; et. lia. }
      { splits; ss; eauto with ord_step. }
      i. mDesAll. des; clarify.
      steps. astop. steps.
      force_l. eexists. steps.
      hret _; ss. iPureIntro. esplits; ss.
      f_equal. f_equal. lia.
      Unshelve. all: ss. all: try exact 0.
  Qed.

End SIMMODSEM.

author: alxest

repo: CCR

save_path: github-repos/coq/alxest-CCR


text:
(** * Facts about Architecture Generation *)

Require Import common.CoqLib.
Require Import common.GlobalFacts.
Require Import common.StateAndErrorMonad.
Require Import common.ListLib.
Require Import common.proofs.StateAndErrorMonadTactics.
Require Import common.proofs.ListMonadFacts.
Require Import common.proofs.SetoidListFacts.
Require Import common.proofs.ListPlusFacts.

Require Import sitpn.SitpnLib.
Require Import sitpn.SitpnFacts.

Require Import hvhdl.AbstractSyntax.
Require Import hvhdl.WellDefinedDesign.
Require Import hvhdl.proofs.AbstractSyntaxFacts.

Require Import transformation.Sitpn2HVhdl.
Require Import transformation.Sitpn2HVhdlUtils.
Require Import transformation.proofs.SInvTactics.

(** ** Facts about the generation of PDIs *)

Section GenPDIsFacts.

  (** *** Facts about the [build_pdi] function *)

  Lemma build_pdi_inv_beh :
    forall {sitpn} {p : P sitpn} {pinfo n s v s'},
      build_pdi p pinfo n s = OK v s' ->
      beh s = beh s'.
  Proof. intros; pattern s, s'; solve_sinv_pattern. Qed.

  Lemma build_pdi_inv_γ :
    forall {sitpn} {p : P sitpn} {pinfo n s v s'},
      build_pdi p pinfo n s = OK v s' ->
      γ s = γ s'.
  Proof. intros; pattern s, s'; solve_sinv_pattern. Qed.

  Lemma build_pdi_inv_inc_nextid :
    forall {sitpn} {p : P sitpn} {pinfo n s v s'},
      build_pdi p pinfo n s = OK v s' ->
      nextid s <= nextid s'.
  Proof. intros; pattern s, s'; solve_sinv_pattern.
         all: try (unfold Transitive; intros; lia).
         cbn; minv EQ5; auto.
  Qed.

  (** *** Facts about the [generate_pdi] function *)

  Lemma pdi_ex_Peq_equiv :
    forall sitpn (x y : P sitpn) s,
      Peq x y ->
      ((exists id__p g__p i__p o__p,
           InA Pkeq (x, id__p) (p2pdi (γ s))
           /\ InCs (cs_comp id__p Petri.place_id g__p i__p o__p) (beh s))
       <-> (exists id__p g__p i__p o__p,
               InA Pkeq (y, id__p) (p2pdi (γ s))
               /\ InCs (cs_comp id__p Petri.place_id g__p i__p o__p) (beh s))).
  Proof.
    intros; split;
      (edestruct 1 as (id__p, (g__p, (i__p, (o__p, (InA_a, InCs_)))));
       exists id__p, g__p, i__p, o__p; split; [ eauto with setoidl | assumption ]).
  Qed.

  Lemma gen_pdi_pdi_ex :
    forall sitpn (n : nat) (a : P sitpn) (s1 : Sitpn2HVhdlState sitpn)
           (x : unit) (s2 : Sitpn2HVhdlState sitpn),
      generate_pdi a n s1 = OK x s2 ->
      exists id__p g__p i__p o__p,
        InA Pkeq (a, id__p) (p2pdi (γ s2)) /\ InCs (cs_comp id__p Petri.place_id g__p i__p o__p) (beh s2).
  Proof.
    intros *; intros e; minv e.
    all: do 4 eexists; split; [ eauto with setoidl | left; eauto ].
  Qed.

  Lemma gen_pdi_pdi_ex_inv :
    forall sitpn (n : nat) (a : P sitpn) (s1 : Sitpn2HVhdlState sitpn) (x : unit) (s2 : Sitpn2HVhdlState sitpn),
      generate_pdi a n s1 = OK x s2 ->
      forall b,
        (exists id__p g__p i__p o__p,
            InA Pkeq (b, id__p) (p2pdi (γ s1)) /\ InCs (cs_comp id__p Petri.place_id g__p i__p o__p) (beh s1)) ->
        exists id__p g__p i__p o__p,
          InA Pkeq (b, id__p) (p2pdi (γ s2)) /\ InCs (cs_comp id__p Petri.place_id g__p i__p o__p) (beh s2).
  Proof.
    intros *; intros e b; destruct (Peqdec a b) as [Peq_ab | nPeq_ab].

    (* CASE [Peq a b], implies [Q a s' <-> Q b s']. *)
    - rewrite <- (pdi_ex_Peq_equiv sitpn a b s1 Peq_ab).
      rewrite <- (pdi_ex_Peq_equiv sitpn a b s2 Peq_ab).
      intro; eapply gen_pdi_pdi_ex; eauto.

    (* CASE [~Peq a b], then nevermind the new entry [(a, id__p)] and new
     PDI in [(beh s2)]. *)
    - monadInv e; monadInv EQ; monadInv EQ2; monadInv EQ.
      rewrite (getv_inv_state EQ4); minv EQ1.
      match goal with
      | [ H: build_pdi _ _ _ ?s = _ |- _ ] => set (s1' := s) in H
      end.
      change (γ s1) with (γ s1'); change (beh s1) with (beh s1').
      rewrite (build_pdi_inv_beh EQ0); rewrite (build_pdi_inv_γ EQ0); minv EQ3.
      edestruct 1 as (id__p, (g__p, (i__p, (o__p, (InA_a, InCs_))))).
      exists id__p, g__p, i__p, o__p; split; [ eauto 1 with setoidl | right; assumption ].
  Qed.

  (** *** Facts about the [generate_pdis] function *)

  Lemma gen_pdis_pdi_ex :
    forall (sitpn : Sitpn) (b : P sitpn -> nat) (s : Sitpn2HVhdlState sitpn) v s' p,
      generate_pdis b s = OK v s' ->
      Sig_in_List (lofPs s) ->
      (exists id__p g__p i__p o__p,
          InA Pkeq (p, id__p) (p2pdi (γ s'))
          /\ InCs (cs_comp id__p Petri.place_id g__p i__p o__p) (beh s')).
  Proof.
    intros *; intros e; minv e. intros SIL_lofPs.
    pattern p, s'.
    eapply iter_prop_A_state with (eqA := Peq); eauto.

    (* Proves that [Peq a b] implies [Q a s' <-> Q b s']. *)
    - eapply pdi_ex_Peq_equiv.

    (* Proves that [∀ a, f a s = OK v s' -> Q a s'] where [f]
     is [generate_pdi] here. *)
    - cbn; intros x; eapply gen_pdi_pdi_ex.

    (* Proves that property [Q] is invariant. *)
    - simpl; intros x; eapply gen_pdi_pdi_ex_inv with (n := b x).

    (* Proves that *)
    - eapply SIL_forall_A; eauto.
  Qed.

End GenPDIsFacts.

(** ** Facts about the generation of TDIs *)

Section GenTDIsFacts.

  (** *** Facts about the [build_tdi] function *)

  Lemma build_tdi_inv_beh :
    forall {sitpn} {t : T sitpn} {tinfo s v s'},
      build_tdi t tinfo s = OK v s' ->
      beh s = beh s'.
  Proof. intros; pattern s, s'; solve_sinv_pattern. Qed.

  Lemma build_tdi_inv_inc_nextid :
    forall {sitpn} {t : T sitpn} {tinfo s v s'},
      build_tdi t tinfo s = OK v s' ->
      nextid s <= nextid s'.
  Proof. intros; pattern s, s'; solve_sinv_pattern.
         match goal with
         | EQ: _ _ = OK _ _ |- _ =>
             cbn; minv EQ; auto
         end.
  Qed.

  (** *** Facts about the [generate_tdis] function *)

  Lemma gen_tdis_pdi_ex :
    forall (sitpn : Sitpn) (s : Sitpn2HVhdlState sitpn) v s' p,
      generate_tdis s = OK v s' ->
      (exists id__p g__p i__p o__p,
          InA Pkeq (p, id__p) (p2pdi (γ s))
          /\ InCs (cs_comp id__p Petri.place_id g__p i__p o__p) (beh s)) ->
      (exists id__p g__p i__p o__p,
          InA Pkeq (p, id__p) (p2pdi (γ s'))
          /\ InCs (cs_comp id__p Petri.place_id g__p i__p o__p) (beh s')).
  Proof. intros *; intros H; pattern s, s'; solve_sinv_pattern.
         match goal with
         | [ EQ: OK _ _ = OK _ _ |- _ ] =>
             inversion EQ; subst; cbn
         end;
         destruct 1 as [id__p [g__p [i__p [o__p [InA_ InCs_] ] ] ] ].
         exists id__p, g__p, i__p, o__p; split; [ assumption | (right; assumption) ].
  Qed.

End GenTDIsFacts.

(** ** Facts about the [generate_architecture] function *)

Section GenArchiFacts.

  Lemma gen_arch_inv_lofPs :
    forall {sitpn mm s v s'},
      @generate_architecture sitpn mm s = OK v s' ->
      lofPs s = lofPs s'.
  Proof. intros *; intros H; pattern s, s'; solve_sinv_pattern. Qed.

  Lemma gen_arch_inv_lofTs :
    forall {sitpn mm s v s'},
      @generate_architecture sitpn mm s = OK v s' ->
      lofTs s = lofTs s'.
  Proof. intros *; intros H; pattern s, s'; solve_sinv_pattern. Qed.

  Lemma gen_arch_inv_sil_lofTs :
    forall {sitpn mm s v s'},
      @generate_architecture sitpn mm s = OK v s' ->
      Sig_in_List (lofTs s) -> Sig_in_List (lofTs s').
  Proof. intros *; intros H; pattern s, s'; solve_sinv_pattern. Qed.

  Lemma gen_archi_pdi_ex :
    forall (sitpn : Sitpn) (b : P sitpn -> nat) (s : Sitpn2HVhdlState sitpn) v s' p,
      generate_architecture b s = OK v s' ->
      Sig_in_List (lofPs s) ->
      (exists id__p g__p i__p o__p,
          InA Pkeq (p, id__p) (p2pdi (γ s'))
          /\ InCs (cs_comp id__p Petri.place_id g__p i__p o__p) (beh s')).
  Proof.
    intros *; intros e; monadInv e; intros SIL_lofPs.
    eapply gen_tdis_pdi_ex; eauto.
    eapply gen_pdis_pdi_ex; eauto.
  Qed.

  Lemma gen_archi_nodup_cids2 :
    forall (sitpn : Sitpn) (b : P sitpn -> nat)
           (s : Sitpn2HVhdlState sitpn) v s',
      generate_architecture b s = OK v s' ->
      (forall id__c, In id__c (get_cids (beh s)) -> id__c < nextid s) /\ NoDup (get_cids (beh s)) ->
      (forall id__c, In id__c (get_cids (beh s')) -> id__c < nextid s') /\ NoDup (get_cids (beh s')).
  Proof.
    intros *; intros H Pstart; generalize Pstart; pattern s, s'; solve_sinv_pattern.
    (* Solves nextid subgoals. *)
    all: try (match goal with
              | [ EQ: _ = OK _ ?s  |- (_) _ ?s ] =>
                  cbn; minv EQ; destruct 1;
                  (split; [ intros; eapply Nat.lt_lt_succ_r; eauto | assumption ])
              end).
    (* new tdi in beh *)
    - cbn; match_and_minv constr:(@get_nextid sitpn); match_and_minv constr:(@OK).
      destruct 1 as [ Inlt4 NoDup4 ]; split; rewrite get_cids_app; cbn.
      destruct 1 as [ eq_idc | ]; [ rewrite <- eq_idc | eauto ].
      match goal with
      | H: build_tdi _ _ _ = _ |- _ => shelf_state H; unfold lt
      end.
      match goal with
      | [ s := _ : Sitpn2HVhdlState _ |- S (nextid ?s') <= _ ] =>
          change (S (nextid s')) with (nextid s)
      end.
      eapply build_tdi_inv_inc_nextid; eauto.
      constructor; eauto.
      let build_tdi_eq := (get_meq build_tdi) in
      rewrite <- (build_tdi_inv_beh build_tdi_eq); simpl.
      match goal with
      |  |- ~In ?ns _ => intros In6; apply (Nat.lt_irrefl ns)
      end;
      eapply (proj1 (P1 P0)); eauto.

    (* new pdi in beh *)
    - let EQ_get_nextid := get_meq (@get_nextid sitpn) in
      let EQ_OK := get_meq (@OK (Sitpn2HVhdlState sitpn)) in
      cbn; minv EQ_get_nextid; minv EQ_OK.
      destruct 1 as [ Inlt4 NoDup4 ]; split; rewrite get_cids_app; cbn.
      destruct 1 as [ eq_idc | ]; [ rewrite <- eq_idc | eauto ].
      match goal with
      | H: build_pdi _ _ _ _ = _ |- _ => shelf_state H; unfold lt
      end.
      match goal with
      | [ s := _ : Sitpn2HVhdlState _ |- S (nextid ?s') <= _ ] =>
          change (S (nextid s')) with (nextid s)
      end.
      eapply build_pdi_inv_inc_nextid; eauto.
      constructor; eauto.
      let EQ_build_pdi := get_meq build_pdi in
      rewrite <- (build_pdi_inv_beh EQ_build_pdi); simpl.
      match goal with
      |  |- ~In ?ns _ =>
           intros In6; apply (Nat.lt_irrefl ns)
      end; eapply (proj1 (P0 P)); eauto.
  Qed.

  Lemma gen_archi_nodup_cids :
    forall (sitpn : Sitpn) (b : P sitpn -> nat)
           (s : Sitpn2HVhdlState sitpn) v s',
      generate_architecture b s = OK v s' ->
      (forall id__c, In id__c (get_cids (beh s)) -> id__c < nextid s) ->
      NoDup (get_cids (beh s)) ->
      NoDup (get_cids (beh s')).
  Proof. intros; eapply gen_archi_nodup_cids2; eauto. Qed.

End GenArchiFacts.

author: viampietro

repo: ver-hilecop

save_path: github-repos/coq/viampietro-ver-hilecop


text:
Require Import List Relation_Operators Operators_Properties Lia.
Import ListNotations.

Require Import Undecidability.StringRewriting.Reductions.CM2_HALT_to_SSTS01.SR2ab.

Require Import ssreflect.

Set Default Goal Selector "!".

Lemma sym_eq_dec (x y: Symbol) : {x = y} + {x <> y}.
Proof. by do 3 (decide equality). Qed.

Lemma stepI {srs u v a b c d s t} :
  s = (u ++ a :: b :: v) -> t = (u ++ c :: d :: v) -> In ((a, b), (c, d)) srs ->
  step srs s t.
Proof. move=> -> ->. by constructor. Qed.

Lemma multi_step_appI {srs u v s t} : multi_step srs s t -> multi_step srs (u ++ s ++ v) (u ++ t ++ v).
Proof.
  elim; [| move=> *; by apply: rt_refl | move=> *; apply: rt_trans; by eassumption ].
  move=> {}s {}t [] u' v' > ?.
  apply /rt_step /(stepI (u := u ++ u') (v := v' ++ v)); last by eassumption.
  all: by rewrite -?app_assoc.
Qed.

Lemma multi_step_applI {srs u s t} : multi_step srs s t -> multi_step srs (u ++ s) (u ++ t).
Proof. move=> /multi_step_appI => /(_ u []). by rewrite ?app_nil_r. Qed.

Lemma multi_step_apprI {srs v s t} : multi_step srs s t -> multi_step srs (s ++ v) (t ++ v).
Proof. by move=> /multi_step_appI => /(_ [] v). Qed.

author: uds-psl

repo: coq-synthetic-incompleteness


Require Import Crypto.Specific.Framework.SynthesisFramework.
Require Import Crypto.Specific.montgomery64_2e192m2e64m1_3limbs.CurveParameters.

Module P <: PrePackage.
  Definition package : Tag.Context.
  Proof. make_Synthesis_package curve extra_prove_mul_eq extra_prove_square_eq. Defined.
End P.

Module Export S := PackageSynthesis P.


text:
(* * Second-Order Peano Arithmetic *)

Require Import PeanoNat Lia Vector.
From Undecidability.SOL Require Import SOL PA2.
From Undecidability.Shared.Libs.PSL Require Import Vectors VectorForall.
From Undecidability.SOL.Util Require Import Syntax Subst Tarski.
From Undecidability.Synthetic Require Import Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts.
Require Import Undecidability.Shared.Dec.

Import VectorNotations SubstNotations SOLNotations PA2Notations.

Set Default Proof Using "Type".

Arguments Vector.cons {_} _ {_} _, _ _ _ _.

Unset Implicit Arguments.

(* ** Discreteness and Enumerability *)

#[global]
Instance PA2_funcs_signature_eq_dec :
  eq_dec PA2_funcs_signature.
Proof.
  intros x y. unfold dec. decide equality.
Qed.

#[global]
Instance PA2_preds_signature_eq_dec :
  eq_dec PA2_preds_signature.
Proof.
  intros [] []. now left.
Qed.

Definition L_PA2_funcs (n : nat) := List.cons Zero (List.cons Succ (List.cons Plus (List.cons Mult List.nil))).
Definition L_PA2_preds (n : nat) := List.cons Eq List.nil.

#[global]
Instance PA2_funcs_enum :
  list_enumerator__T L_PA2_funcs PA2_funcs.
Proof.
  intros []; exists 0; firstorder.
Qed.

#[global]
Instance PA2_preds_enum :
  list_enumerator__T L_PA2_preds PA2_preds.
Proof.
  intros []; exists 0; firstorder.
Qed.

Lemma PA2_form_enumerable :
  enumerable__T form.
Proof.
  apply form_enumerable.
  - apply list_enumerable__T_enumerable. exists L_PA2_funcs. apply PA2_funcs_enum.
  - apply list_enumerable__T_enumerable. exists L_PA2_preds. apply PA2_preds_enum.
  - apply enumT_binop.
  - apply enumT_quantop.
Qed.

Lemma PA2_enumerable :
  enumerable PA2.
Proof.
  exists (fun n => List.nth n (List.map Some PA2_L) None). intros phi. split.
  - intros H. repeat destruct H as [<-|H].
    now exists 0. now exists 1. now exists 2. now exists 3. now exists 4.
    now exists 5. now exists 6. now exists 7. now exists 8. easy.
  - intros [n H]. assert (forall x y : form, Some x = Some y -> x = y) as Some_inj by congruence.
    do 9 try destruct n as [|n]; try apply Some_inj in H as <-. 1-9: firstorder.
    destruct n; cbn in H; congruence.
Qed.

Lemma PA2_closed :
  forall phi, PA2 phi -> closed phi.
Proof.
  intros phi H. repeat destruct H as [<-|H]; cbv; firstorder.
  destruct (Nat.eq_dec ar 1) as [->|]. left; firstorder. right; firstorder.
Qed.

(* Since PA2 is closed, we can characterize validity without requiring to
    satisfy phi in the same environment as PA2 *)
Lemma PA2_valid_alternative phi :
  PA2 ⊨ phi <-> forall M, M ⊨ PA2 -> M ⊨ phi.
Proof.
  split.
  - intros H1 M H2 rho. apply H1. intros psi H3. repeat destruct H3 as [<-|H3];
    try apply H2; try easy; clear; firstorder.
  - intros H1 M rho H2. apply H1. intros psi H3. repeat destruct H3 as [<-|H3]; intros rho'.
    apply (H2 ax_eq_refl). 2: apply (H2 ax_eq_symm). 3: apply (H2 ax_zero_succ). 4: apply (H2 ax_succ_inj).
    5: apply (H2 ax_add_zero). 6: apply (H2 ax_add_rec). 7: apply (H2 ax_mul_zero). 8: apply (H2 ax_mul_rec).
    9: apply (H2 ax_ind). 10: easy. all: clear; firstorder.
Qed.

(* ** Helper Lemmas for working with models of PA2 *)

Section Model.

  Variable M : Model.

  Definition empty_PA2_env M : env (M_domain M) := ⟨ fun n => i_f (M_domain M) Zero ([]) , fun n ar v => i_f (M_domain M) Zero ([]), fun n ar v => True ⟩.

  Hypothesis M_correct : M ⊨ PA2 .

  Notation "'izero'" := (@i_f _ _ (M_domain M) (M_interp M) Zero ([])).
  Notation "'iσ' x" := (@i_f _ _ (M_domain M) (M_interp M) Succ ([x])) (at level 37).
  Notation "x 'i⊕' y" := (@i_f _ _ (M_domain M) (M_interp M) Plus ([x ; y])) (at level 39).
  Notation "x 'i⊗' y" := (@i_f _ _ (M_domain M) (M_interp M) Mult ([x ; y])) (at level 38).
  Notation "x 'i==' y" := (@i_P _ _ (M_domain M)  (M_interp M) Eq ([x ; y])) (at level 40).

  Lemma eq_reflexive x :
    x i== x.
  Proof using M_correct. revert x. apply (M_correct ax_eq_refl ltac:(firstorder) (empty_PA2_env _)). Qed.

  Lemma eq_symm x y :
    x i== y -> y i== x.
  Proof using M_correct. apply (M_correct ax_eq_symm ltac:(firstorder) (empty_PA2_env _)). Qed.

  Lemma zero_succ' x :
    izero i== iσ x -> False.
  Proof using M_correct. apply (M_correct ax_zero_succ ltac:(firstorder) (empty_PA2_env _)). Qed.

  Lemma succ_inj' x y :
    iσ x i== iσ y -> x i== y.
  Proof using M_correct. apply (M_correct ax_succ_inj ltac:(firstorder) (empty_PA2_env _)). Qed.

  (* Simplify induction axiom by removing the vector *)
  Lemma induction (P : M_domain M -> Prop) :
    P izero -> (forall x, P x -> P (iσ x)) -> forall x, P x.
  Proof using M_correct.
    pose (P' := fun v : vec _ 1 => P (Vector.hd v)).
    change (P' ([izero]) -> (forall x, P' ([x]) -> P' ([iσ x])) -> forall x, P' ([x])).
    apply (M_correct ax_ind ltac:(firstorder) (empty_PA2_env _)).
  Qed.

  Lemma case_analysis x :
    x = izero \/ exists x', x = iσ x'.
  Proof using M_correct.
    revert x. apply induction.
    - now left.
    - intros x _. right. now exists x.
  Qed.

  Lemma eq_sem x y :
    x i== y <-> x = y.
  Proof using M_correct.
    split.
    - revert x y. apply (induction (fun x => forall y, x i== y -> x = y)).
      + intros y H. destruct (case_analysis y) as [->|[y' ->]].
        * reflexivity.
        * now apply zero_succ' in H.
      + intros x IH y H. destruct (case_analysis y) as [->|[y' ->]].
        * now apply eq_symm, zero_succ' in H.
        * rewrite (IH y'). reflexivity. now apply succ_inj'.
    - intros ->. apply eq_reflexive.
  Qed.

  Lemma zero_succ x :
    izero = iσ x -> False.
  Proof using M_correct. intros H%eq_sem. now apply (zero_succ' x). Qed.

  Lemma succ_inj x y :
    iσ x = iσ y -> x = y.
  Proof using M_correct. intros H%eq_sem. now apply eq_sem, (succ_inj' x y). Qed.

  Lemma add_zero x :
    izero i⊕ x = x.
  Proof using M_correct. apply eq_sem, (M_correct ax_add_zero ltac:(firstorder) (empty_PA2_env _)). Qed.

  Lemma add_rec x y :
    iσ x i⊕ y = iσ (x i⊕ y).
  Proof using M_correct. apply eq_sem, (M_correct ax_add_rec ltac:(firstorder) (empty_PA2_env _)). Qed.

  Lemma mul_zero x :
    izero i⊗ x = izero.
  Proof using M_correct. apply eq_sem, (M_correct ax_mul_zero ltac:(firstorder) (empty_PA2_env _)). Qed.

  Lemma mul_rec x y :
    iσ x i⊗ y = y i⊕ (x i⊗ y).
  Proof using M_correct. apply eq_sem, (M_correct ax_mul_rec ltac:(firstorder) (empty_PA2_env _)). Qed.

  (* Convert from nat to this model *)

  Fixpoint to_domain n : M_domain M := match n with
    | 0 => izero
    | S n => iσ (to_domain n)
  end.

  Lemma to_domain_add x y :
    to_domain (x + y) = to_domain x i⊕ to_domain y.
  Proof using M_correct.
    revert y. induction x; intros; cbn.
    - symmetry. apply add_zero.
    - rewrite add_rec. now repeat f_equal.
  Qed.

  Lemma to_domain_mul x y :
    to_domain (x * y) = to_domain x i⊗ to_domain y.
  Proof using M_correct.
    revert y. induction x; intros; cbn.
    - symmetry. apply mul_zero.
    - rewrite mul_rec. rewrite to_domain_add. now repeat f_equal.
  Qed.

  Lemma to_domain_injective x x' :
    to_domain x = to_domain x' -> x = x'.
  Proof using M_correct.
    revert x'. induction x; destruct x'.
    - reflexivity.
    - now intros H%zero_succ.
    - intros H. symmetry in H. now apply zero_succ in H.
    - intros H%succ_inj. now rewrite (IHx x').
  Qed.

End Model.

(* ** Standard Model *)

Section StandardModel.

  Definition std_interp_f (f : syms) : vec nat (ar_syms f) -> nat :=
    match f with
      | Zero => fun _ => 0
      | Succ => fun v => S (Vector.hd v)
      | Plus => fun v => Vector.hd v + Vector.hd (Vector.tl v)
      | Mult => fun v => Vector.hd v * Vector.hd (Vector.tl v)
    end.

  Definition std_interp_P (P : preds) : vec nat (ar_preds P) -> Prop :=
    match P with
      | Eq => fun v => Vector.hd v = Vector.hd (Vector.tl v)
    end.

  Instance I_nat : interp nat := {| i_f := std_interp_f ; i_P := std_interp_P |}.

  Definition Standard_Model : Model := {|
    M_domain := nat ;
    M_interp := I_nat
  |}.

  Lemma std_model_correct :
    Standard_Model ⊨ PA2.
  Proof.
    intros phi H. repeat try destruct H as [<-|H]; hnf; cbn; try congruence.
    intros rho P H IH n. induction n; auto. easy.
  Qed.

End StandardModel.

(* ** Signature Embedding *)

(* We can embed the PA2 signature into the formula and translate to
    an arbitrary signature. *)

Section EmbedSignature.

  Definition Σf := PA2_funcs_signature.
  Definition Σp := PA2_preds_signature.
  Context {Σf' : funcs_signature}.
  Context {Σp' : preds_signature}.
  Context {D : Type}.
  Context {I : @interp Σf Σp D}.
  Context {I' : @interp Σf' Σp' D}.

  (* We assume that the PA2 functions and predicates are inside the
     environment at

        xO = Position of zero
        xS = Position of succ
        xA = Position of add
        xA + 1 = Position of mul

     Replace function and predicate symbols with the corresponding
     variable and shift the existing variables.
  *)

  Fixpoint embed_term xO xS xA (t : @term Σf) : @term Σf' := match t with
    | var_indi x => var_indi x
    | func (sym Zero) v => func (@var_func _ xO 0) (Vector.map (embed_term xO xS xA) v)
    | func (sym Succ) v => func (@var_func _ xS 1) (Vector.map (embed_term xO xS xA) v)
    | func (sym Plus) v => func (@var_func _ xA 2) (Vector.map (embed_term xO xS xA) v)
    | func (sym Mult) v => func (@var_func _ (S xA) 2) (Vector.map (embed_term xO xS xA) v)
    | func (@var_func _ x 0) v => if Compare_dec.le_lt_dec xO x then func (@var_func _ (S x) 0) (Vector.map (embed_term xO xS xA) v) else func (@var_func _ x 0) (Vector.map (embed_term xO xS xA) v)
    | func (@var_func _ x 1) v => if Compare_dec.le_lt_dec xS x then func (@var_func _ (S x) 1) (Vector.map (embed_term xO xS xA) v) else func (@var_func _ x 1) (Vector.map (embed_term xO xS xA) v)
    | func (@var_func _ x 2) v => if Compare_dec.le_lt_dec xA x then func (@var_func _ (S (S x)) 2) (Vector.map (embed_term xO xS xA) v) else func (@var_func _ x 2) (Vector.map (embed_term xO xS xA) v)
    | func (@var_func _ x ar) v => func (@var_func _ x ar) (Vector.map (embed_term xO xS xA) v)
  end.

  Fixpoint embed_form xO xS xA xEq (phi : @form Σf Σp _) : @form Σf' Σp' _ := match phi with
    | fal => fal
    | atom (pred Eq) v => atom (@var_pred _ xEq 2) (Vector.map (embed_term xO xS xA) v)
    | atom (@var_pred _ x 2) v => if Compare_dec.le_lt_dec xEq x then atom (@var_pred _ (S x) 2) (Vector.map (embed_term xO xS xA) v) else atom (@var_pred _ x 2) (Vector.map (embed_term xO xS xA) v)
    | atom (@var_pred _ x ar) v => atom (@var_pred _ x ar) (Vector.map (embed_term xO xS xA) v)
    | bin op phi psi => bin op (embed_form xO xS xA xEq phi) (embed_form xO xS xA xEq psi)
    | quant_indi op phi => quant_indi op (embed_form xO xS xA xEq phi)
    | quant_func op 0 phi => quant_func op 0 (embed_form (S xO) xS xA xEq phi)
    | quant_func op 1 phi => quant_func op 1 (embed_form xO (S xS) xA xEq phi)
    | quant_func op 2 phi => quant_func op 2 (embed_form xO xS (S xA) xEq phi)
    | quant_func op ar phi => quant_func op ar (embed_form xO xS xA xEq phi)
    | quant_pred op 2 phi => quant_pred op 2 (embed_form xO xS xA (S xEq) phi)
    | quant_pred op ar phi => quant_pred op ar (embed_form xO xS xA xEq phi)
  end.

  Definition pred n := match n with 0 => 0 | S n => n end.

  (* Predicate that states that rho' contains the PA2 signature inserted at
      positions xO, xS, xA and xEq, and matches up with rho. *)
  Definition env_contains_PA2 (rho rho' : env D) xO xS xA xEq :=
    (forall n, get_indi rho n = get_indi rho' n) /\
    (forall n ar, get_func rho' n ar = match ar with
        | 0 => match Compare_dec.lt_eq_lt_dec n xO with inleft (left _) => get_func rho n 0 | inleft (right _) => @i_f _ _ D I Zero | inright _ => get_func rho (pred n) 0 end
        | 1 => match Compare_dec.lt_eq_lt_dec n xS with inleft (left _) => get_func rho n 1 | inleft (right _) => @i_f _ _ D I Succ | inright _ => get_func rho (pred n) 1 end
        | 2 => if Nat.eq_dec n xA then @i_f _ _ D I Plus else match Compare_dec.lt_eq_lt_dec n (S xA) with inleft (left _) => get_func rho n 2 | inleft (right _) => @i_f _ _ D I Mult | inright _ => get_func rho (pred (pred n)) 2 end
        | ar => get_func rho n ar
      end) /\
    (forall n ar, get_pred rho' n ar = match ar with
        | 2 => match Compare_dec.lt_eq_lt_dec n xEq with inleft (left _) => get_pred rho n 2 | inleft (right _) => @i_P _ _ D I Eq | inright _ => get_pred rho (pred n) 2 end
        | ar => get_pred rho n ar
      end).

  Local Arguments Nat.eq_dec : simpl never.
  Local Arguments Compare_dec.lt_eq_lt_dec : simpl never.

  Ltac solve_env E :=
    try destruct Compare_dec.lt_eq_lt_dec as [[|]|]; try lia;
    try destruct Nat.eq_dec; try lia; cbn; try rewrite E;
    try destruct Compare_dec.lt_eq_lt_dec as [[|]|]; try lia;
    try destruct Nat.eq_dec; try lia;
    try destruct Compare_dec.lt_eq_lt_dec as [[|]|]; try lia;
    try destruct Nat.eq_dec; try lia; cbn; try rewrite E;
    try destruct Compare_dec.lt_eq_lt_dec as [[|]|]; try lia;
    try destruct Nat.eq_dec; try lia.

  Lemma env_contains_PA2_scons_i rho rho' xO xS xA xEq d :
    env_contains_PA2 rho rho' xO xS xA xEq -> env_contains_PA2 ⟨d .: get_indi rho, get_func rho, get_pred rho⟩ ⟨d .: get_indi rho', get_func rho', get_pred rho'⟩ xO xS xA xEq.
  Proof.
    intros E. split. 2: apply E. intros []. reflexivity. apply E.
  Qed.

  Lemma env_contains_PA2_scons_f {rho rho' xO xS xA xEq ar} (f : vec D ar -> D) :
    env_contains_PA2 rho rho' xO xS xA xEq ->
    match ar with
      | 0 => env_contains_PA2 ⟨get_indi rho, f .: get_func rho, get_pred rho⟩ ⟨get_indi rho', f .: get_func rho', get_pred rho'⟩ (S xO) xS xA xEq
      | 1 => env_contains_PA2 ⟨get_indi rho, f .: get_func rho, get_pred rho⟩ ⟨get_indi rho', f .: get_func rho', get_pred rho'⟩ xO (S xS) xA xEq
      | 2 => env_contains_PA2 ⟨get_indi rho, f .: get_func rho, get_pred rho⟩ ⟨get_indi rho', f .: get_func rho', get_pred rho'⟩ xO xS (S xA) xEq
      | ar => env_contains_PA2 ⟨get_indi rho, f .: get_func rho, get_pred rho⟩ ⟨get_indi rho', f .: get_func rho', get_pred rho'⟩ xO xS xA xEq
    end.
  Proof.
    intros E. unfold econs, econs_func, econs_ar. destruct ar as [|[|[]]];
    split; try apply E; split; try apply E; destruct E as [_ [E2 _]];
    intros [|[|[]]] [|[|[]]]; solve_env E2; reflexivity.
  Qed.

  Lemma env_contains_PA2_scons_p {rho rho' xO xS xA xEq ar} (P : vec D ar -> Prop) :
    env_contains_PA2 rho rho' xO xS xA xEq ->
    match ar with
      | 2 => env_contains_PA2 ⟨get_indi rho, get_func rho, P .: get_pred rho⟩ ⟨get_indi rho', get_func rho', P .: get_pred rho'⟩ xO xS xA (S xEq)
      | _ => env_contains_PA2 ⟨get_indi rho, get_func rho, P .: get_pred rho⟩ ⟨get_indi rho', get_func rho', P .: get_pred rho'⟩ xO xS xA xEq
    end.
  Proof.
    intros E. unfold econs, econs_func, econs_ar. destruct ar as [|[|[]]];
    split; try apply E; split; try apply E; destruct E as [_ [_ E3]];
    intros [|[|[]]] [|[|[]]]; solve_env E3; reflexivity.
  Qed.

  Lemma embed_term_correct rho rho' xO xS xA xEq t :
    env_contains_PA2 rho rho' xO xS xA xEq -> @eval Σf Σp D I rho t = @eval Σf' Σp' D I' rho' (embed_term xO xS xA t).
  Proof.
    intros E. induction t; cbn.
    - apply E.
    - destruct E as [_ [E2 _]]. apply map_ext_forall in IH. destruct ar as [|[|[]]];
      try destruct Compare_dec.le_lt_dec; cbn; rewrite E2;
      try destruct Compare_dec.lt_eq_lt_dec as [[|]|]; try lia;
      try destruct Nat.eq_dec; try lia; now rewrite map_map, IH.
    - destruct E as [_ [E2 _]]. apply map_ext_forall in IH. destruct f; cbn in *;
      rewrite E2; destruct Compare_dec.lt_eq_lt_dec as [[|]|]; try lia;
      try destruct Nat.eq_dec; try lia; now rewrite map_map, IH.
  Qed.

  Lemma embed_form_correct rho rho' xO xS xA xEq phi :
    env_contains_PA2 rho rho' xO xS xA xEq -> @sat Σf Σp D I rho phi <-> @sat Σf' Σp' D I' rho' (embed_form xO xS xA xEq phi).
  Proof.
    revert rho rho' xO xS xA xEq. induction phi; intros rho rho' xO xS xA xEq E; cbn.
    - reflexivity.
    - rename t into v. assert (map (@eval Σf Σp D I rho) v = map (fun t => @eval Σf' Σp' D I' rho' (embed_term xO xS xA t)) v) as Hv'.
      { clear p. induction v. reflexivity. cbn; f_equal.
        apply (embed_term_correct _ _ _ _ _ _ _ E). apply IHv. }
      destruct E as [_ [_ E3]]. destruct p; cbn.
      + destruct ar as [|[|[]]];
        try destruct Compare_dec.le_lt_dec; cbn; rewrite E3;
        try destruct Compare_dec.lt_eq_lt_dec as [[|]|]; try lia;
        now rewrite map_map, Hv'.
      + destruct P; cbn in *. rewrite E3.
        destruct Compare_dec.lt_eq_lt_dec as [[|]|]; try lia.
        now rewrite map_map, Hv'.
    - specialize (IHphi1 rho rho' xO xS xA xEq E);
      specialize (IHphi2 rho rho' xO xS xA xEq E).
      destruct b; tauto.
    - destruct q.
      + split; intros H d; eapply IHphi. 2,4: apply (H d). all: now apply env_contains_PA2_scons_i.
      + split; intros [d H]; exists d; eapply IHphi. 2,4: apply H. all: now apply env_contains_PA2_scons_i.
    - destruct q; destruct n as [|[|[]]]; split.
      1-8: intros H f; eapply IHphi; try apply (H f); try apply H; now apply (env_contains_PA2_scons_f f).
      all: intros [f H]; exists f; eapply IHphi; try apply (H f); try apply H; now apply (env_contains_PA2_scons_f f).
    - destruct q; destruct n as [|[|[]]]; split.
      1-8: intros H P; eapply IHphi; try apply (H P); try apply H; now apply (env_contains_PA2_scons_p P).
      all: intros [P H]; exists P; eapply IHphi; try apply (H P); try apply H; now apply (env_contains_PA2_scons_p P).
  Qed.

End EmbedSignature.

(* Now we can translate satisfiability and validity for arbitrary models
    over arbitrary signatures to PA2 models. *)

Section PA2ValidSatTranslation.

  Context `{Σf' : funcs_signature}.
  Context `{Σp' : preds_signature}.

  (* Encode axioms into formula *)
  Definition PA2_form :=
    ax_eq_refl ∧ ax_eq_symm ∧ ax_zero_succ ∧ ax_succ_inj ∧ ax_add_zero ∧ ax_add_rec ∧ ax_mul_zero ∧ ax_mul_rec ∧ ax_ind.

  Lemma PA2_Model_sat_PA2_form M :
    forall rho, (M, rho) ⊨ PA2 <-> (M, rho) ⊨ PA2_form.
  Proof.
    intros rho. split.
    - intros M_correct. repeat split; apply M_correct; repeat (try (left; reflexivity); try right).
    - intros H. intros phi H1. repeat destruct H1 as [<-|H1]; try apply H; try easy.
  Qed.

  Lemma PA2_model_valid_iff_model_valid (phi : @form PA2_funcs_signature PA2_preds_signature _) :
    (forall M rho, (M, rho) ⊨ PA2 -> (M, rho) ⊨ phi) <-> (forall M' rho, (M', rho) ⊨ (∀f(0) ∀f(1) ∀f(2) ∀f(2) ∀p(2) (embed_form 0 0 0 0 (PA2_form ~> phi)))).
  Proof.
    split.
    - intros H M' rho fO fS fM fA pE.
      pose (I := @B_I PA2_funcs_signature PA2_preds_signature _
                    (fun f => match f with Zero => fO | Succ => fS | Plus => fA | Mult => fM end)
                    (fun P => match P with Eq => pE end )).
      pose (M := {| M_domain := M_domain M' ; M_interp := I |}).
      eapply (embed_form_correct rho).
      + cbn. split. 2: split. now intros n. now intros [|[|[]]] [|[|[]]]. now intros [] [|[|[]]].
      + intros H_PA2. apply (H M), PA2_Model_sat_PA2_form, H_PA2.
    - intros H M rho M_correct.
      pose (I' := {| i_f _ _ := @i_f _ _ _ (M_interp M) Zero ([]) ; i_P _ _ := True |} ).
      pose (M' := {| M_domain := M_domain M ; M_interp := I' |}).
      pose (zero' := @i_f _ _ _ (M_interp M) Zero);  pose (succ := @i_f _ _ _ (M_interp M) Succ); pose (plus := @i_f _ _ _ (M_interp M) Plus);  pose (mult := @i_f _ _ _ (M_interp M) Mult); pose (equal := @i_P _ _ _ (M_interp M) Eq).
      specialize (H M' rho zero' succ mult plus equal).
      eapply embed_form_correct in H.
      + apply H. apply -> PA2_Model_sat_PA2_form. apply M_correct.
      + split. 2: split. now intros n. now intros [|[|[]]] [|[|[]]]. now intros [] [|[|[]]].
  Qed.

  Lemma PA2_model_sat_iff_model_sat (phi : @form PA2_funcs_signature PA2_preds_signature _) :
    (exists M rho, (M, rho) ⊨ PA2 /\ (M, rho) ⊨ phi) <-> (exists M' rho, (M', rho) ⊨ (∃f(0) ∃f(1) ∃f(2) ∃f(2) ∃p(2) (embed_form 0 0 0 0 (PA2_form ∧ phi)))).
  Proof.
    split.
    - intros [M [rho H]].
      pose (I' := @B_I Σf' Σp' _ (fun f _ => @i_f _ _ _ (M_interp M) Zero ([])) (fun P _ => True )).
      pose (M' := {| M_domain := M_domain M ; M_interp := I' |}).
      exists M', rho.
      exists (@i_f _ _ _ (M_interp M) Zero), (@i_f _ _ _ (M_interp M) Succ), (@i_f _ _ _ (M_interp M) Mult), (@i_f _ _ _ (M_interp M) Plus), (@i_P _ _ _ (M_interp M) Eq).
      eapply (embed_form_correct rho).
      + cbn. split. 2: split. now intros n. now intros [|[|[]]] [|[|[]]]. now intros [] [|[|[]]].
      + split. now apply -> PA2_Model_sat_PA2_form. apply H.
    - intros [M' [rho [fO [fS [fM [fA [pE H]]]]]]]; cbn -[embed_form] in H.
      pose (I := @B_I PA2_funcs_signature PA2_preds_signature _
                    (fun f => match f with Zero => fO | Succ => fS | Plus => fA | Mult => fM end)
                    (fun P => match P with Eq => pE end )).
      pose (M := {| M_domain := M_domain M' ; M_interp := I |}).
      exists M, rho. eapply (embed_form_correct rho) in H.
      + split. apply PA2_Model_sat_PA2_form, H. apply H.
      + split. 2: split. now intros n. now intros [|[|[]]] [|[|[]]]. now intros [] [|[|[]]].
  Qed.

  Definition embed_PA2 phi := ∀f(0) ∀f(1) ∀f(2) ∀f(2) ∀p(2) (@embed_form Σf' Σp' 0 0 0 0 (PA2_form ~> phi)).

  Lemma PA2_sat_iff_empty_theory_sat (phi : @form PA2_funcs_signature PA2_preds_signature _) :
    PA2 ⊨ phi <-> (fun _ => False) ⊨ embed_PA2 phi.
  Proof.
    split.
    - intros H M rho HM. now apply PA2_model_valid_iff_model_valid.
    - intros H M. apply PA2_model_valid_iff_model_valid. intros M' rho. now apply (H M').
  Qed.

End PA2ValidSatTranslation.


text:
(*

  Copyright 2014 Cornell University
  Copyright 2015 Cornell University
  Copyright 2016 Cornell University
  Copyright 2017 Cornell University

  This file is part of VPrl (the Verified Nuprl project).

  VPrl is free software: you can redistribute it and/or modify
  it under the terms of the GNU General Public License as published by
  the Free Software Foundation, either version 3 of the License, or
  (at your option) any later version.

  VPrl is distributed in the hope that it will be useful,
  but WITHOUT ANY WARRANTY; without even the implied warranty of
  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  GNU General Public License for more details.

  You should have received a copy of the GNU General Public License
  along with VPrl.  If not, see <http://www.gnu.org/licenses/>.

  Websites: http://nuprl.org/html/verification/
            http://nuprl.org/html/Nuprl2Coq
            https://github.com/vrahli/NuprlInCoq

  Authors: Vincent Rahli

*)

Require Export bar_induction_cterm.
Require Export subst_tacs.
Require Export per_props_equality.
Require Export lsubstc_vars.

(**

  Bar induction, where
    X is the proposition
    B is the bar
    ext(s,n,t) = \m. if m=n then t else s m
<<
   H |- squash (X 0 (\v.let _ := v in bot))

     By bar_induction B i a s x m n t

     H, n:nat, s: nat_n -> CNTerm |- B n s in Type(i)        // B is a well-formed predicate on finite sequences
     H, s: nat -> CNTerm |- squash(exists n:nat. B n s)      // B is a bar
     H, n:nat, s: nat_n -> CNTerm, m: squash(B n s) |- X n s         // Base case: the conclusion is true at the bar
     H, n:nat, s: nat_n -> CNTerm, x: (forall m: CNTerm. X (n + 1) (ext(s,n,m))) |- X n s // induction case
>>

*)

Definition rule_bar_induction_nout3 {o}
           (f X B e : @NTerm o)
           (s n m v x : NVar)
           (i : nat)
           (H : barehypotheses) :=
  mk_rule
    (mk_bseq H (mk_conclax (mk_squash (mk_apply2 X mk_zero (cbv_emseq v)))))
    [ mk_bseq (snoc (snoc H (mk_hyp n mk_tnat))
                    (mk_hyp s (mk_natk2nout (mk_var n))))
              (mk_conclax (mk_member (mk_apply2 B (mk_var n) (mk_var s)) (mk_uni i))),
      mk_bseq (snoc H (mk_hyp s mk_nat2nout))
              (mk_conclax (mk_squash
                             (mk_exists mk_tnat
                                        n
                                        (mk_apply2 B (mk_var n) (mk_var s))))),
      mk_bseq (snoc (snoc (snoc H (mk_hyp n mk_tnat))
                          (mk_hyp s (mk_natk2nout (mk_var n))))
                    (mk_hyp m (mk_squash (mk_apply2 B (mk_var n) (mk_var s)))))
              (mk_concl (mk_apply2 X (mk_var n) (mk_var s)) e),
      mk_bseq (snoc (snoc (snoc H (mk_hyp n mk_tnat))
                          (mk_hyp s (mk_natk2nout (mk_var n))))
                    (mk_hyp x (mk_all
                                 mk_nout
                                 m
                                 (mk_squash (mk_apply2 X (mk_plus1 (mk_var n)) (mk_update_seq (mk_var s) (mk_var n) (mk_var m) v))))))
              (mk_conclax (mk_apply2 X (mk_var n) (mk_var s)))
    ]
    [].

Lemma rule_bar_induction_nout3_true {o} :
  forall lib (f X B e : @NTerm o)
         (s n m v x : NVar)
         (i : nat)
         (H : @barehypotheses o)
         (dxv : x <> v)
         (dsv : s <> v)
         (dnv : n <> v)
         (dnv : m <> v)
         (dnm : n <> m)
         (dsm : s <> m)
         (nnB : !LIn n (free_vars B))
         (nsB : !LIn s (free_vars B)),
    rule_true lib (rule_bar_induction_nout3 f X B e s n m v x i H).
Proof.
  unfold rule_bar_induction_nout3, rule_true, closed_type_baresequent, closed_extract_baresequent; simpl.
  intros.
  clear cargs.

  (* We prove the well-formedness of things *)
  destseq; allsimpl.
  dLin_hyp.
  destruct Hyp  as [wf1 hyp_wfd].
  destruct Hyp0 as [wf2 hyp_bar].
  destruct Hyp1 as [wf3 hyp_imp].
  destruct Hyp2 as [wf4 hyp_ind].
  destseq; allsimpl; proof_irr; GC.

  unfold closed_extract; simpl.

  exists (@covered_axiom o (nh_vars_hyps H)).

  (* We prove some simple facts on our sequents *)
  assert (s <> n
          # s <> x
          # n <> x
          # !LIn x (free_vars X)
          # !LIn s (free_vars X)
          # !LIn n (free_vars X)
          # !LIn m (free_vars X)
          # !LIn x (vars_hyps H)
          # !LIn s (vars_hyps H)
          # !LIn n (vars_hyps H)) as vhyps.

  { clear hyp_wfd hyp_bar hyp_ind hyp_imp.
    dwfseq.
    sp; GC;
    try (complete (discover; allapply @subset_hs_vars_hyps; sp)). }

  destruct vhyps as [ nsn vhyps ].
  destruct vhyps as [ nsx vhyps ].
  destruct vhyps as [ nnx vhyps ].
  destruct vhyps as [ nxX vhyps ].
  destruct vhyps as [ nsX vhyps ].
  destruct vhyps as [ nnX vhyps ].
  destruct vhyps as [ nmX vhyps ].
  destruct vhyps as [ nxH vhyps ].
  destruct vhyps as [ nsH nnH ].
  (* done with proving these simple facts *)

  vr_seq_true.
  lsubst_tac.

  autorewrite with slow in *.
  clear_irr.
  clear_wf_hyps.

  rw @tequality_mkc_squash.
  rw @member_mkc_squash.

  assert (!LIn n (dom_csub s1)) as nns1.
  { apply similarity_dom in sim; repnd.
    rw sim0; auto. }

  assert (!LIn n (dom_csub s2)) as nns2.
  { apply similarity_dom in sim; repnd.
    rw sim; auto. }

  assert (!LIn s (dom_csub s1)) as nss1.
  { apply similarity_dom in sim; repnd.
    rw sim0; auto. }

  assert (!LIn s (dom_csub s2)) as nss2.
  { apply similarity_dom in sim; repnd.
    rw sim; auto. }

  assert (!LIn x (dom_csub s1)) as nxs1.
  { apply similarity_dom in sim; repnd.
    rw sim0; auto. }

  assert (!LIn x (dom_csub s2)) as nxs2.
  { apply similarity_dom in sim; repnd.
    rw sim; auto. }

  assert (wf_term B) as wB.
  { clear hyp_wfd.
    allrw @wf_member_iff2.
    allrw <- @wf_apply2_iff; sp.
  }

  assert (cover_vars B s1 # cover_vars B s2) as cB.
  { clear hyp_wfd.
    allrw @covered_member.
    allrw @covered_apply2; repnd.
    allrw @vars_hyps_snoc; allsimpl.
    apply covered_snoc_implies in ct4; auto.
    apply covered_snoc_implies in ct4; auto.
    dands.
    - eapply s_cover_typ1;[exact ct4|exact sim].
    - eapply s_cover_typ1;[exact ct4|].
      apply similarity_sym in sim;[exact sim|]; auto.
  }
  destruct cB as [cB1 cB2].

  assert (forall k seq1 seq2 s1a s2a cB1 cB2,
            similarity lib s1a s2a H
            -> hyps_functionality lib s1a H
            -> eq_kseq_nout lib seq1 seq2 k
            -> tequality
                 lib
                 (mkc_apply2 (lsubstc B wB s1a cB1) (mkc_nat k) seq1)
                 (mkc_apply2 (lsubstc B wB s2a cB2) (mkc_nat k) seq2)) as Bfunc.
  { introv sim0 hf0 eqk.
    vr_seq_true in hyp_wfd.
    pose proof (hyp_wfd
                  (snoc (snoc s1a (n,mkc_nat k)) (s,seq1))
                  (snoc (snoc s2a (n,mkc_nat k)) (s,seq2)))
      as h; clear hyp_wfd.
    repeat (autodimp h hyp).

    { apply hyps_functionality_snoc2; simpl; auto.

      { introv equ' sim'.
        apply similarity_snoc in sim'; simpl in sim'.
        exrepnd; subst; ginv; inj.
        eapply tequality_respects_alphaeqc_left;
          [apply alphaeqc_sym; apply lsubstc_mk_natk2nout_sp2; auto;
           apply similarity_dom in sim'3; repnd; rw sim'0; auto
          |].
        eapply tequality_respects_alphaeqc_right;
          [apply alphaeqc_sym; apply lsubstc_mk_natk2nout_sp2; auto;
           apply similarity_dom in sim'3; repnd; rw sim'3; auto
          |].
        allrw @lsubstc_mkc_tnat.
        apply equality_int_nat_implies_cequivc in sim'1.
        eapply tequality_respects_cequivc_right;
          [apply implies_cequivc_natk2nout; exact sim'1|].
        eauto 3 with slow.
      }

      apply hyps_functionality_snoc2; simpl; auto.

      introv equ' sim'.
      allrw @lsubstc_mkc_tnat.
      apply tnat_type.
    }

    { assert (@wf_term o (mk_natk2nout (mk_var n))) as wfn.
      { apply wf_term_mk_natk2nout; auto. }
      assert (cover_vars (mk_natk2nout (mk_var n)) (snoc s1a (n,mkc_nat k))) as cvn.
      { apply cover_vars_mk_natk2nout.
        apply cover_vars_var.
        rw @dom_csub_snoc.
        rw in_snoc; simpl; sp. }
      sim_snoc.
      dands; auto.

      { pose proof (cover_vars_mk_tnat s1a) as cvs1.
        pose proof (@wf_tnat o) as wftn.
        sim_snoc.
        dands; auto.
        allrw @lsubstc_mkc_tnat.
        apply equality_in_tnat_nat.
      }

      eapply alphaeqc_preserving_equality;
        [|apply alphaeqc_sym;
           apply lsubstc_mk_natk2nout_sp2; auto];
        auto.
      apply similarity_dom in sim0; repnd.
      rw sim1; auto.
    }

    exrepnd.
    lsubst_tac.
    apply tequality_in_uni_implies_tequality in h0; auto.
    apply member_if_inhabited in h1.
    auto.
  }

  pose proof (bar_induction_cterm_meta2
                lib
                (fun_sim_eq lib s1 H B wB)
                (fun_sim_eq lib s1 H X w0)
                (lsubstc B wB s1 cB1)
                (lsubstc X w0 s1 c0)
                v)
    as bi.

  repeat (autodimp bi hyp);
    [idtac
    |idtac
    |idtac
    |pose proof (bi (lsubstc X w0 s2 c5) (cbv_emseqc v)) as h;
      allrw <- @mkc_zero_eq;
      repeat (autodimp h hyp);[apply eq_kseq_nout_0|idtac|repnd; dands; complete auto];
      exists s2 c5;
      dands; complete auto
    ].

  - intros seq1 iss.

    vr_seq_true in hyp_bar.
    pose proof (hyp_bar
                  (snoc s1 (s,seq1))
                  (snoc s1 (s,seq1)))
      as hf; clear hyp_bar.
    repeat (autodimp hf hyp).

    { apply hyps_functionality_snoc2; simpl; auto.

      introv equ' sim'.
      allrw @lsubstc_mk_nat2nout.
      apply type_nat2nout.
    }

    { assert (@wf_term o mk_nat2nout) as wfn.
      { apply wf_term_mk_nat2nout; auto. }
      assert (cover_vars mk_nat2nout s1) as cvn.
      { apply cover_vars_mk_nat2nout. }
      sim_snoc.
      dands; auto.
      { eapply similarity_refl; eauto. }
      allrw @lsubstc_mk_nat2nout.
      auto.
    }

    exrepnd.
    clear hf0.
    lsubst_tac.
    apply equality_in_mkc_squash in hf1; exrepnd.
    clear hf0 hf2.
    allunfold @mk_exists.
    lsubst_tac.
    allrw @lsubstc_mkc_tnat.
    apply inhabited_product in hf1; exrepnd.
    clear hf2.

    apply member_tnat_implies_computes in hf1; exrepnd.

    exists k.
    introv eqs fse.
    unfold fun_sim_eq in fse; exrepnd; subst.

    repeat substc_lsubstc_vars3.
    lsubst_tac.
    clear_wf_hyps.
    proof_irr.

    pose proof (Bfunc k seq1 (seq2kseq seq1 k v) s1 s1 cB1 cB1) as h.
    repeat (autodimp h hyp); eauto 3 with slow.
    { eapply similarity_refl; eauto. }

    eapply inhabited_type_cequivc in hf3;
      [|apply implies_cequivc_apply2;
         [apply cequivc_refl
         |apply computes_to_valc_implies_cequivc;eauto
         |apply cequivc_refl]
      ].

    eapply inhabited_type_tequality in hf3;[|eauto].

    dands; auto.

  - intros k seq1 iss sb C seq2 eqs fse.
    clear iss.
    unfold fun_sim_eq in fse; exrepnd; subst.
    unfold nout_on_seq in sb.
    rename fse0 into sim0.

    assert (cover_vars B s0) as cB0.
    { eapply similarity_cover_vars;[exact sim0|]; auto. }

    pose proof (sb (lsubstc B wB s0 cB0) seq2) as h; clear sb.
    repeat (autodimp h hyp).
    { exists s0 cB0; dands; auto. }
    repnd.

    unfold inhabited_type in h0; exrepnd.
    rename h1 into mem.
    rename h into teq.

    vr_seq_true in hyp_imp.
    pose proof (hyp_imp
                  (snoc (snoc (snoc s1 (n,mkc_nat k)) (s,seq1)) (m,mkc_axiom))
                  (snoc (snoc (snoc s0 (n,mkc_nat k)) (s,seq2)) (m,mkc_axiom)))
      as hf.
    repeat (autodimp hf hyp).

    { apply hyps_functionality_snoc2; simpl; auto.

      { introv equ' sim'.
        apply similarity_snoc in sim'; simpl in sim'.
        exrepnd; subst; ginv; inj.
        apply similarity_snoc in sim'3; simpl in sim'3.
        exrepnd; subst; ginv; inj.
        lsubst_tac.
        allrw @lsubstc_mkc_tnat.
        apply equality_int_nat_implies_cequivc in sim'2.
        eapply alphaeqc_preserving_equality in sim'1;
          [|apply lsubstc_mk_natk2nout_sp2; auto].
        apply tequality_mkc_squash.
        eapply tequality_respects_cequivc_right;
          [apply implies_cequivc_apply2;
            [apply cequivc_refl
            |exact sim'2
            |apply cequivc_refl]
          |].
        auto.
      }

      apply hyps_functionality_snoc2; simpl; auto.

      { introv equ' sim'.
        apply similarity_snoc in sim'; simpl in sim'.
        exrepnd; subst; ginv; cpx.
        assert (!LIn n (dom_csub s2a)) as nns2a.
        { apply similarity_dom in sim'3; repnd.
          rw sim'3; auto. }
        eapply tequality_respects_alphaeqc_left;
          [apply alphaeqc_sym;
            apply lsubstc_mk_natk2nout_sp2; auto
          |].
        eapply tequality_respects_alphaeqc_right;
          [apply alphaeqc_sym;
            apply lsubstc_mk_natk2nout_sp2; auto
          |].
        rw @lsubstc_mkc_tnat in sim'1.
        apply equality_int_nat_implies_cequivc in sim'1.
        eapply tequality_respects_cequivc_right;
          [apply implies_cequivc_natk2nout; exact sim'1|].
        eauto 3 with slow.
      }

      apply hyps_functionality_snoc2; simpl; auto.

      introv equ' sim'.
      allrw @lsubstc_mkc_tnat.
      apply tnat_type.
    }

    { assert (wf_term (mk_squash (mk_apply2 B (mk_var n) (mk_var s)))) as wfn.
      { apply wf_squash.
        apply wf_apply2; eauto 3 with slow. }
      assert (cover_vars (mk_squash (mk_apply2 B (mk_var n) (mk_var s))) (snoc (snoc s1 (n,mkc_nat k)) (s,seq1))) as cvn.
      { apply cover_vars_squash.
        apply cover_vars_apply2.
        repeat (rw @cover_vars_var_iff).
        repeat (rw @dom_csub_snoc); simpl.
        repeat (rw in_snoc).
        dands; tcsp.
        repeat (apply cover_vars_snoc_weak); auto. }
      sim_snoc.
      dands; auto.

      { assert (@wf_term o (mk_natk2nout (mk_var n))) as wfk.
        { apply wf_term_mk_natk2nout; auto. }
        assert (cover_vars (mk_natk2nout (mk_var n)) (snoc s1 (n,mkc_nat k))) as cvk.
        { apply cover_vars_mk_natk2nout.
          apply cover_vars_var_iff.
          repeat (rw @dom_csub_snoc); simpl.
          repeat (rw in_snoc); sp. }
        sim_snoc.
        dands; auto.

        { assert (@wf_term o mk_tnat) as wft.
          { eauto 3 with slow. }
          assert (cover_vars mk_tnat s1) as cvt.
          { apply cover_vars_mk_tnat. }
          sim_snoc.
          dands; auto.
          allrw @lsubstc_mkc_tnat.
          eauto 3 with slow.
        }

        eapply alphaeqc_preserving_equality;
          [|apply alphaeqc_sym; apply lsubstc_mk_natk2nout_sp2; auto].
        auto.
      }

      { lsubst_tac; auto.
        apply member_mkc_squash.
        exists t; auto.
      }
    }

    exrepnd.
    lsubst_tac.
    apply inhabited_type_if_equality in hf1.
    auto.

  - intros k seq1 iss ind C seq2 eqs fse.
    clear iss.
    unfold fun_sim_eq in fse; exrepnd; subst.

    vr_seq_true in hyp_ind.

    pose proof (hyp_ind
                  (snoc (snoc (snoc s1 (n,mkc_nat k)) (s,seq1)) (x,lam_axiom))
                  (snoc (snoc (snoc s0 (n,mkc_nat k)) (s,seq2)) (x,lam_axiom)))
      as hf; clear hyp_ind.
    repeat (autodimp hf hyp).

    { apply hyps_functionality_snoc2; simpl; auto.

      { introv equ' sim'.
        apply similarity_snoc in sim'; simpl in sim'.
        exrepnd; subst; ginv; inj.
        apply similarity_snoc in sim'3; simpl in sim'3.
        exrepnd; subst; ginv; inj.
        allunfold @mk_all.
        lsubst_tac.
        allrw @lsubstc_mkc_tnat.
        allrw @lsubstc_mk_nout.
        apply equality_int_nat_implies_cequivc in sim'2.
        eapply alphaeqc_preserving_equality in sim'1;
          [|apply lsubstc_mk_natk2nout_sp2; auto].

        apply tequality_function; dands.
        { apply type_mkc_nout. }
        introv en.
        repeat substc_lsubstc_vars3.
        lsubst_tac.
        apply equality_in_nout in en.
        exrepnd; spcast.

        apply tequality_mkc_squash.

        eapply tequality_respects_cequivc_left;
          [apply cequivc_sym;
            apply implies_cequivc_apply2;
            [apply cequivc_refl
            |apply cequivc_lsubstc_mk_plus1_sp1;auto
            |apply cequivc_lsubstc_mk_update_seq_sp0;auto]
          |].

        assert (!LIn n (dom_csub s2a0)) as nin2.
        { apply similarity_dom in sim'4; repnd.
          rw sim'4; auto. }

        assert (!LIn s (dom_csub s2a0)) as nis2.
        { apply similarity_dom in sim'4; repnd.
          rw sim'4; auto. }

        eapply tequality_respects_cequivc_right;
          [apply cequivc_sym;
            apply implies_cequivc_apply2;
            [apply cequivc_refl
            |apply cequivc_lsubstc_mk_plus1_sp2; auto;
             apply cequivc_sym;exact sim'2
            |apply cequivc_lsubstc_mk_update_seq_sp3;auto;
             apply cequivc_sym;eauto
            ]
          |].

        eapply tequality_respects_cequivc_left;
          [apply cequivc_sym;
            apply implies_cequivc_apply2;
            [apply cequivc_refl
            |apply cequivc_refl
            |apply implies_cequivc_update_seq_nout;eauto
            ]
          |].

        eapply tequality_respects_cequivc_right;
          [apply cequivc_sym;
            apply implies_cequivc_apply2;
            [apply cequivc_refl
            |apply cequivc_refl
            |apply implies_cequivc_update_seq_nout;eauto
            ]
          |].

        pose proof (ind (cterm2cnterm u en1)) as h; clear ind.
        unfold nout_on_upd_seq in h.
        unfold nout_on_seq in h; repnd.
        allunfold @cnout_cterm.
        allrw @cnterm2cterm2cnterm.

        pose proof (h (lsubstc X w0 s2a0 c27) (update_seq_nout t2 k u v)) as q; clear h.
        repeat (autodimp q hyp); repnd; auto;[|].
        { apply eq_kseq_nout_update2; auto. }
        { exists s2a0 c27; dands; auto. }
      }

      apply hyps_functionality_snoc2; simpl; auto.

      { introv equ' sim'.
        apply similarity_snoc in sim'; simpl in sim'.
        exrepnd; subst; ginv; inj.
        assert (!LIn n (dom_csub s2a)) as nns2a.
        { apply similarity_dom in sim'3; repnd.
          rw sim'3; auto. }
        eapply tequality_respects_alphaeqc_left;
          [apply alphaeqc_sym;
            apply lsubstc_mk_natk2nout_sp2; auto
          |].
        eapply tequality_respects_alphaeqc_right;
          [apply alphaeqc_sym;
            apply lsubstc_mk_natk2nout_sp2; auto
          |].
        rw @lsubstc_mkc_tnat in sim'1.
        apply equality_int_nat_implies_cequivc in sim'1.
        eapply tequality_respects_cequivc_right;
          [apply implies_cequivc_natk2nout; exact sim'1|].
        eauto 3 with slow.
      }

      apply hyps_functionality_snoc2; simpl; auto.

      introv equ' sim'.
      allrw @lsubstc_mkc_tnat.
      apply tnat_type.
    }

    { assert (wf_term (mk_all mk_nout m
                              (mk_squash
                                 (mk_apply2 X (mk_plus1 (mk_var n))
                                            (mk_update_seq (mk_var s) (mk_var n) (mk_var m) v))))) as wa.
      { apply wf_function; auto.
        apply wf_squash.
        apply wf_apply2; auto. }
      assert (cover_vars (mk_all mk_nout m
                              (mk_squash
                                 (mk_apply2 X (mk_plus1 (mk_var n))
                                            (mk_update_seq (mk_var s) (mk_var n) (mk_var m) v))))
                         (snoc (snoc s1 (n, mkc_nat k)) (s, seq1))) as ca.
      { apply cover_vars_function; dands; auto.
        { apply cover_vars_mk_tnat. }
        apply cover_vars_upto_squash.
        apply cover_vars_upto_apply2; dands; auto.
        { repeat (rw @csub_filter_snoc).
          allrw memvar_singleton.
          boolvar;tcsp;GC;[].
          repeat (apply cover_vars_upto_snoc_weak).
          apply cover_vars_upto_csub_filter_disjoint; auto.
          apply disjoint_singleton_r; auto. }
        { apply cover_vars_upto_add; dands; eauto 3 with slow.
          repeat (rw @csub_filter_snoc).
          allrw memvar_singleton.
          boolvar;tcsp;GC;[].
          apply cover_vars_upto_var; simpl.
          repeat (rw @dom_csub_snoc).
          repeat (rw in_snoc;simpl).
          sp. }
        { unfold mk_update_seq.
          apply cover_vars_upto_lam.
          rw @csub_filter_swap.
          rw <- @csub_filter_app_r; simpl.
          repeat (rw @csub_filter_snoc).
          allrw memvar_cons; simpl.
          boolvar;tcsp;GC;[].
          apply cover_vars_upto_int_eq; dands.
          { apply cover_vars_upto_var; simpl.
            repeat (rw @dom_csub_snoc).
            repeat (rw in_snoc;simpl).
            sp. }
          { apply cover_vars_upto_var; simpl.
            repeat (rw @dom_csub_snoc).
            repeat (rw in_snoc;simpl).
            sp. }
          { apply cover_vars_upto_var; simpl.
            repeat (rw @dom_csub_snoc).
            repeat (rw in_snoc;simpl).
            sp. }
          { apply cover_vars_upto_apply; dands.
            { apply cover_vars_upto_var; simpl.
              repeat (rw @dom_csub_snoc).
              repeat (rw in_snoc;simpl).
              sp. }
            { apply cover_vars_upto_var; simpl.
              repeat (rw @dom_csub_snoc).
              repeat (rw in_snoc;simpl).
              sp. }
          }
        }
      }
      sim_snoc.
      dands; auto.

      { assert (@wf_term o (mk_natk2nout (mk_var n))) as wfk.
        { apply wf_term_mk_natk2nout; auto. }
        assert (cover_vars (mk_natk2nout (mk_var n)) (snoc s1 (n,mkc_nat k))) as cvk.
        { apply cover_vars_mk_natk2nout.
          apply cover_vars_var_iff.
          repeat (rw @dom_csub_snoc); simpl.
          repeat (rw in_snoc); sp. }
        sim_snoc.
        dands; auto.

        { assert (@wf_term o mk_tnat) as wft.
          { eauto 3 with slow. }
          assert (cover_vars mk_tnat s1) as cvt.
          { apply cover_vars_mk_tnat. }
          sim_snoc.
          dands; auto.
          allrw @lsubstc_mkc_tnat.
          eauto 3 with slow.
        }

        eapply alphaeqc_preserving_equality;
          [|apply alphaeqc_sym; apply lsubstc_mk_natk2nout_sp2; auto].
        auto.
      }

      { unfold mk_all.
        lsubst_tac.
        allrw @lsubstc_mk_nout.
        apply equality_in_function.
        dands; auto.

        { apply type_mkc_nout. }

        { introv en.
          repeat substc_lsubstc_vars3.
          lsubst_tac.
          apply equality_in_nout in en; exrepnd; spcast.

          apply tequality_mkc_squash.

          eapply tequality_respects_cequivc_left;
            [apply cequivc_sym;
              apply implies_cequivc_apply2;
              [apply cequivc_refl
              |apply cequivc_lsubstc_mk_plus1_sp1;auto
              |apply cequivc_lsubstc_mk_update_seq_sp0;auto]
            |];[].

          eapply tequality_respects_cequivc_right;
            [apply cequivc_sym;
              apply implies_cequivc_apply2;
              [apply cequivc_refl
              |apply cequivc_lsubstc_mk_plus1_sp2; auto;
               apply cequivc_sym;exact sim'2
              |apply cequivc_lsubstc_mk_update_seq_sp0;auto]
            |];[].

          eapply tequality_respects_cequivc_left;
            [apply cequivc_sym;
              apply implies_cequivc_apply2;
              [apply cequivc_refl
              |apply cequivc_refl
              |apply implies_cequivc_update_seq_nout;eauto
              ]
            |].

          eapply tequality_respects_cequivc_right;
            [apply cequivc_sym;
              apply implies_cequivc_apply2;
              [apply cequivc_refl
              |apply cequivc_refl
              |apply implies_cequivc_update_seq_nout;eauto
              ]
            |].

          pose proof (ind (cterm2cnterm u en1)) as h; clear ind.
          unfold nout_on_upd_seq in h.
          unfold nout_on_seq in h; repnd.
          allunfold @cnout_cterm.
          allrw @cnterm2cterm2cnterm.

          pose proof (h (lsubstc X w0 s1 c0) (update_seq_nout seq1 k u v)) as q; clear h.
          repeat (autodimp q hyp); repnd; auto;[|].
          { apply eq_kseq_nout_update2; auto.
            eapply equality_refl; eauto. }
          { exists s1 c0; dands; auto.
            eapply similarity_refl; eauto. }
        }

        { introv en.
          repeat substc_lsubstc_vars3.
          eapply equality_respects_cequivc_left;
            [apply cequivc_sym;apply cequivc_mkc_apply_lam_axiom|].
          eapply equality_respects_cequivc_right;
            [apply cequivc_sym;apply cequivc_mkc_apply_lam_axiom|].

          clear_wf_hyps.
          proof_irr.
          lsubst_tac.

          apply equality_in_mkc_squash; dands; spcast;
          try (apply computes_to_valc_refl; eauto 3 with slow).

          apply equality_in_nout in en; exrepnd; spcast.

          eapply inhabited_type_cequivc;
            [apply cequivc_sym;
              apply implies_cequivc_apply2;
              [apply cequivc_refl
              |apply cequivc_lsubstc_mk_plus1_sp1;auto
              |apply cequivc_lsubstc_mk_update_seq_sp0;auto]
            |];[].

          eapply inhabited_type_cequivc;
            [apply cequivc_sym;
              apply implies_cequivc_apply2;
              [apply cequivc_refl
              |apply cequivc_refl
              |apply implies_cequivc_update_seq_nout;eauto
              ]
            |];[].

          pose proof (ind (cterm2cnterm u en1)) as h; clear ind.
          unfold nout_on_upd_seq in h.
          unfold nout_on_seq in h; repnd.
          allunfold @cnout_cterm.
          allrw @cnterm2cterm2cnterm.

          pose proof (h (lsubstc X w0 s1 c0) (update_seq_nout seq1 k u v)) as q; clear h.
          repeat (autodimp q hyp); repnd; auto;[|].
          { apply eq_kseq_nout_update2; auto.
            eapply equality_refl; eauto. }
          { exists s1 c0; dands; auto.
            eapply similarity_refl; eauto. }
        }
      }
    }

    exrepnd.
    lsubst_tac.
    apply inhabited_type_if_equality in hf1.
    dands; auto.
Qed.

(*
*** Local Variables:
*** coq-load-path: ("." "../util/" "../terms/" "../computation/" "../cequiv/" "../per/" "../close/")
*** End:
*)

author: vrahli

repo: NuprlInCoq

save_path: github-repos/coq/vrahli-NuprlInCoq


text:
(************************************************************************)
(*                                                                      *)
(*                Quantitative Hoare Logic for Clight                   *)
(*                                                                      *)
(*  Author: Quentin Carbonneaux (c) 2014              Yale University   *)
(*                                                                      *)
(************************************************************************)

Require Export Core.
Require Import Coqlib.
Require Import AST.
Require Import Clight.
Require Import Memory.
Require Import Events.
Require Import Values.
Require Import Integers.
Require Import Cop.
Require Import Ctypes.
Require Import Globalenvs.
Require Import Maps.
Require Import Smallstep.
Require Import List.

(* quantitative c syntax *)
Definition fid := ident.
Definition var := ident.

Instance QCSyn: BaseSyn fid var expr :=
  { fid_eq := ident_eq }.

Record finfo: Type := mkfinfo {
  fi_name: fid;
  fi_args: list (var * type);
  fi_locals: list (var * type);
  fi_body: stm;
  fi_return: type
}.

Definition genv := Genv.t finfo type.

Program Definition trgenv (ge: genv): Clight.genv :=
  Genv.mkgenv
    (Genv.genv_symb ge)
    (ZMap.init None)
    (Genv.genv_vars ge)
    (Genv.genv_next_pos ge)
    (Genv.genv_symb_range ge)
    _
    (Genv.genv_vars_range ge)
    _
    (Genv.genv_vars_inj ge).
Next Obligation. rewrite ZMap.gi in H. discriminate. Qed.
Next Obligation. rewrite ZMap.gi in H. discriminate. Qed.

Lemma find_symbol_trgenv:
  forall ge id, Genv.find_symbol ge id = Genv.find_symbol (trgenv ge) id.
Proof.
unfold Genv.find_symbol, trgenv; intros.
reflexivity.
Qed.

(* quantitative c semantics *)
Function find_info (ge: genv) (b: block) : option type :=
  match Genv.find_var_info ge b with
  | Some gv => Some gv.(gvar_info)
  | None => None
  end.

Function find_finfo (ge: genv) (f: ident): option finfo :=
  match Genv.find_symbol ge f with
  | Some b => Genv.find_funct_ptr ge b
  | None => None
  end.

Definition lval: Type := ((block * int) * type)%type.
Definition val: Type := (val * type)%type.
Definition stack := temp_env.

Definition eval_expr (ge: genv) (c: conf_) (e: expr) (v: Values.val): Prop :=
  Clight.eval_expr (trgenv ge) empty_env (c_stack c) (c_mem c) e v.

Definition leva_expr (ge: genv) (c: conf_) (e: expr) (p: block * int): Prop :=
  Clight.eval_lvalue (trgenv ge) empty_env (c_stack c) (c_mem c) e (fst p) (snd p).

Definition val_cast (v: val) (ty: type) :=
  sem_cast (fst v) (snd v) ty.

Inductive mem_set_ (ge: genv) (lx: lval) (vy: val) (m: mem): mem -> Prop :=
  | mem_set_intro:
      forall vy' m',
      val_cast vy (snd lx) = Some vy' ->
      assign_loc (snd lx) m (fst (fst lx)) (snd (fst lx)) vy' m' ->
      mem_set_ ge lx vy m m'.

Inductive stack_set_ (ge: genv) (v: var) (vx: val) (s: temp_env): temp_env -> Prop :=
  | stack_set_intro:
      stack_set_ ge v vx s (PTree.set v (fst vx) s).

Inductive castl: list val -> typelist -> list Values.val -> Prop :=
  | castl_nil: castl nil Tnil nil
  | castl_cons:
      forall vx ty v vxs tys vs,
      val_cast vx ty = Some v ->
      castl vxs tys vs ->
      castl (cons vx vxs) (Tcons ty tys) (cons v vs).

Inductive fun_init_ (ge: genv) (f: fid) (args: list val): temp_env -> Prop :=
  | fun_init_intro:
      forall fi vas s,
      find_finfo ge f = Some fi ->
      list_norepet (var_names fi.(fi_args)) ->
      list_disjoint (var_names fi.(fi_args)) (var_names fi.(fi_locals)) ->
      castl args (type_of_params fi.(fi_args)) vas ->
      bind_parameter_temps fi.(fi_args) vas (create_undef_temps fi.(fi_locals)) = Some s ->
      fun_init_ ge f args s.

Inductive fun_ret_ (ge: genv) (f: fid): option val -> option val -> Prop :=
  | fun_ret_some: forall vx vx' fi,
      find_finfo ge f = Some fi ->
      val_cast vx fi.(fi_return) = Some vx' ->
      fun_ret_ ge f (Some vx) (Some (vx', Tvoid))
  | fun_ret_none: forall fi,
      find_finfo ge f = Some fi ->
      fun_ret_ ge f None None.

Function find_func_ (ge: genv) (f: ident) :=
  match find_finfo ge f with
  | Some fi => Some fi.(fi_body)
  | None => None
  end.

Global Instance QCSem: BaseSem genv lval val mem stack QCSyn := {
  find_func := find_func_;
  (* values *)
  val_bool := fun vb b => bool_val (fst vb) (snd vb) = Some b;
  (* memory operations *)
  mem_set := mem_set_;
  stack_set := stack_set_;
  (* functions *)
  fun_init := fun_init_;
  fun_ret := fun_ret_;
  (* expressions *)
  leva := fun ge c e v => leva_expr ge c e (fst v) /\ snd v = typeof e;
  eval := fun ge c e v => eval_expr ge c e (fst v) /\ snd v = typeof e
}.

Definition trevent (e: Core.event) :=
  match e with
  | ecall f => Event_call f
  | eret f => Event_return f
  end.
Definition trtrace := map trevent.

Definition program := AST.program finfo type.
Inductive state: Type :=
  | Initial (main: finfo) (m: mem)
  | Running (main: finfo) (s: Core.stm) (k: Core.cont) (c: Core.conf)
  | Final (code: int).

Inductive step (ge: genv): state -> trace -> state -> Prop :=

  | step_start:
      forall m s main,
      fun_init ge main.(fi_name) nil s ->
      step ge
        (Initial main m) (Event_call main.(fi_name) :: nil)
        (Running main main.(fi_body) kstop (cnf s m))

  | step_core:
      forall main s1 k1 c1 s2 k2 c2 t
             (SEMKSTEP: Core.step ge (s1, k1, c1) t (s2, k2, c2)),
      step ge
        (Running main s1 k1 c1) (trtrace t)
        (Running main s2 k2 c2)

  | step_stop:
      forall main r c code ty
             (RETEVAL: ret_eval ge c main.(fi_name) r (Some (Vint code, ty))),
      step ge
        (Running main (sret r) kstop c) (Event_return main.(fi_name) :: nil)
        (Final code).

Inductive initial_state (p: program): state -> Prop :=
  | initial_state_intro:
      forall main m0,
      let ge := Genv.globalenv p in
      Genv.init_mem p = Some m0 ->
      find_finfo ge p.(prog_main) = Some main ->
      main.(fi_args) = nil ->
      main.(fi_return) = type_int32s ->
      initial_state p (Initial main m0).

Inductive final_state: state -> int -> Prop :=
  | final_state_intro:
      forall code, final_state (Final code) code.

Definition semantics (p: program) :=
  Semantics step (initial_state p) final_state (Genv.globalenv p).

(* Cxlight is receptive to change in events *)
Lemma semantics_receptive:
  forall (p: program), receptive (semantics p).
Proof.
Ltac done := eexists; econstructor; now eauto.

intros. constructor; simpl; intros.
inv H.
  (* step_start *)
  inv H0; done.
  (* step_core *)
  assert (t = T0 -> exists s2, step (Genv.globalenv p) (Running main s0 k1 c1) t2 s2).
  { intros. subst. inv H0.
    change nil with (trtrace T0); done. }
  inversion SEMKSTEP; subst; auto.
    (* return *)
    inv H0.
    change (Event_return kf :: nil)
      with (trtrace (T1 (eret kf))); done.
    (* call *)
    inv H0.
    change (Event_call f :: nil)
      with (trtrace (T1 (ecall f))); done.
  (* step_stop *)
  inv H0; done.

(* single_events (semantics p) *)
red; intros. inv H; simpl; try omega.
inv SEMKSTEP; simpl; try omega.
Qed.

author: academic-archive


text:
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Import Bool NSub NZParity.

(** Some additional properties of [even], [odd]. *)

Module Type NParityProp (Import N : NAxiomsSig')(Import NP : NSubProp N).

Include NZParityProp N N NP.

Lemma odd_pred : forall n, n~=0 -> odd (P n) = even n.
Proof.
 intros. rewrite <- (succ_pred n) at 2 by trivial.
 symmetry. apply even_succ.
Qed.

Lemma even_pred : forall n, n~=0 -> even (P n) = odd n.
Proof.
 intros. rewrite <- (succ_pred n) at 2 by trivial.
 symmetry. apply odd_succ.
Qed.

Lemma even_sub : forall n m, m<=n -> even (n-m) = Bool.eqb (even n) (even m).
Proof.
 intros.
 case_eq (even n); case_eq (even m);
  rewrite <- ?negb_true_iff, ?negb_even, ?odd_spec, ?even_spec;
  intros (m',Hm) (n',Hn).
 exists (n'-m'). now rewrite mul_sub_distr_l, Hn, Hm.
 exists (n'-m'-1).
  rewrite !mul_sub_distr_l, Hn, Hm, sub_add_distr, mul_1_r.
  rewrite two_succ at 5. rewrite <- (add_1_l 1). rewrite sub_add_distr.
  symmetry. apply sub_add.
  apply le_add_le_sub_l.
  rewrite add_1_l, <- two_succ, <- (mul_1_r 2) at 1.
  rewrite <- mul_sub_distr_l. rewrite <- mul_le_mono_pos_l by order'.
  rewrite one_succ, le_succ_l. rewrite <- lt_add_lt_sub_l, add_0_r.
  destruct (le_gt_cases n' m') as [LE|GT]; trivial.
  generalize (double_below _ _ LE). order.
 exists (n'-m'). rewrite mul_sub_distr_l, Hn, Hm.
  apply add_sub_swap.
  apply mul_le_mono_pos_l; try order'.
  destruct (le_gt_cases m' n') as [LE|GT]; trivial.
  generalize (double_above _ _ GT). order.
 exists (n'-m'). rewrite Hm,Hn, mul_sub_distr_l.
  rewrite sub_add_distr. rewrite add_sub_swap. apply add_sub.
  apply succ_le_mono.
  rewrite add_1_r in Hm,Hn. order.
Qed.

Lemma odd_sub : forall n m, m<=n -> odd (n-m) = xorb (odd n) (odd m).
Proof.
 intros. rewrite <- !negb_even. rewrite even_sub by trivial.
 now destruct (even n), (even m).
Qed.

End NParityProp.