Coq Extension

(*
NoConfusion_Foo (P : Type) [indices] (u v : Foo [indices]) :=
 match u, v with
 | Foo x y z, Foo x y z => (x == x' -> y == y' -> z == z' -> P) -> P
 | ...
 | Chalk*, Cheese* => P
 end
*)

(*
noConfusion_Foo (P : Type) [indices] (u v : Foo [indices]) : u == v -> NoConfusion_foo P [indices] u v.
*)

open Univ
open Inductive
open Util
open Coqlib

let ith_univ i = make_univ (make_dirpath [id_of_string"implicit"], i)
let implicit_type i = mkSort (Type (ith_univ i))
let raw_type i = RSort (dummy_loc, RType (Some (ith_univ i)))

let coq_heq_ref = lazy (Coqlib.coq_reference "mkHEq" ["Logic";"JMeq"] "JMeq")

let construct_no_conf_body env ind mind =
  let ctr_types = arities_of_constructors ind mind in
  let n_ctr_types = Array.length ctr_types in
  let n_indices = length (snd mind).mind_arity_ctxt in
  let indices =
    let rec names i = if i > n_indices then [] else RVar (dummy_loc, id_of_string ("e"^string_of_int i)) :: names (i+1) in names 1 in
  let abstract_indices x =
    let rec abs i =
      if i > n_indices
       then x
       else RLambda (dummy_loc, Name (id_of_string ("e"^string_of_int i)), Explicit, RHole (dummy_loc, BinderType Anonymous), abs (i+1)) in
    abs 1 in
  Pretyping.Default.understand Evd.empty env
   (RLambda (dummy_loc, Name (id_of_string "P"), Explicit, raw_type 1,
   abstract_indices
   (RLambda (dummy_loc, Name (id_of_string "u"), Explicit, RApp (dummy_loc, RRef (dummy_loc, IndRef ind), indices),
   (RLambda (dummy_loc, Name (id_of_string "v"), Explicit, RApp (dummy_loc, RRef (dummy_loc, IndRef ind), indices),
     RCases (dummy_loc, MatchStyle, None,
       [(RVar (dummy_loc, (id_of_string "u")), (Anonymous, None));(RVar (dummy_loc, (id_of_string "v")), (Anonymous, None))],
       (Array.to_list (Array.mapi (fun i ty_i ->
         let ctr = (ind, i+1) in
         let ctr_args = constructor_nrealhyps env ctr in
         let rec spread n i = if i = 0 then [] else (PatVar (dummy_loc, Name (id_of_string (n^string_of_int i)))) :: spread n (i-1) in
         let left_patterns = List.rev (spread "i" ctr_args) in
         let right_patterns = List.rev (spread "j" ctr_args) in
         let rec assume_eqs n x = if n > ctr_args
                                   then x
                                   else RProd (dummy_loc, Anonymous, Explicit,
                                        RApp (dummy_loc, RRef (dummy_loc, Lazy.force coq_heq_ref),
                                          [RHole (dummy_loc, BinderType Anonymous); RVar (dummy_loc, id_of_string ("i"^string_of_int n));
                                           RHole (dummy_loc, BinderType Anonymous); RVar (dummy_loc, id_of_string ("j"^string_of_int n))]),
                                        assume_eqs (n+1) x) in
         (dummy_loc, [id_of_string "foo";id_of_string "bar"],
                     [PatCstr (dummy_loc, ctr, left_patterns, Anonymous);PatCstr (dummy_loc, ctr, right_patterns, Anonymous)],
                     RProd (dummy_loc, Anonymous, Explicit,
                       assume_eqs 1 (RVar (dummy_loc, id_of_string "P")), RVar (dummy_loc, id_of_string "P")))) ctr_types) @
        if n_ctr_types = 1
         then []
         else [(dummy_loc, [id_of_string "foo";id_of_string "bar"],
                           [PatVar (dummy_loc, Anonymous);PatVar (dummy_loc, Anonymous)],
                           RVar (dummy_loc, id_of_string "P"))]))))))))

let construct_no_conf_declaration env ind mind =
 DefinitionEntry
  { const_entry_body = construct_no_conf_body env ind mind;
    const_entry_type = None;
    const_entry_opaque = false;
    const_entry_boxed = false }, IsDefinition Definition

let construct_little_no_conf env ind mind little_no_conf no_conf =
  let n_indices = length (snd mind).mind_arity_ctxt in
  let indices =
    let rec names i = if i > n_indices then [] else RVar (dummy_loc, id_of_string ("e"^string_of_int i)) :: names (i+1) in names 1 in
  let abstract_indices x =
    let rec abs i =
      if i > n_indices
       then x
       else RProd (dummy_loc, Name (id_of_string ("e"^string_of_int i)), Explicit, RHole (dummy_loc, BinderType Anonymous), abs (i+1)) in
    abs 1 in
  let little_no_conf_type = Pretyping.Default.understand Evd.empty env 
     (RProd (dummy_loc, Name (id_of_string "P"), Explicit, raw_type 1,
      abstract_indices
     (RProd (dummy_loc, Name (id_of_string "u"), Explicit, RApp (dummy_loc, RRef (dummy_loc, IndRef ind), indices),
     (RProd (dummy_loc, Name (id_of_string "v"), Explicit, RApp (dummy_loc, RRef (dummy_loc, IndRef ind), indices),
     (RProd (dummy_loc, Name (id_of_string "eql"), Explicit,
                          RApp (dummy_loc, RRef (dummy_loc, Lazy.force coq_heq_ref),
                           [RHole (dummy_loc, BinderType Anonymous); RVar (dummy_loc, id_of_string "u");
                            RHole (dummy_loc, BinderType Anonymous); RVar (dummy_loc, id_of_string "v")]),
       RApp (dummy_loc, RRef (dummy_loc, no_conf),
        ([RVar (dummy_loc, id_of_string "P")] @
         indices @
         [RVar (dummy_loc, id_of_string "u");
          RVar (dummy_loc, id_of_string "v")])))))))))) in
  try
    let _ =
    Pfedit.start_proof little_no_conf (Global, DefinitionBody Definition)
      (named_context_val env)
      little_no_conf_type
      (fun _ _ -> ());
    Pfedit.by (tclTHENSEQ
      [intros;
       simplest_elim (mkVar (id_of_string "eql"));
       simplest_elim (mkVar (id_of_string "u"));
       simpl_in_concl;
       Tauto.tauto]) in
    let _,(const,_,_) = Pfedit.cook_proof (fun _ -> ()) in
     Pfedit.delete_current_proof ();
     DefinitionEntry const, IsDefinition Definition
  with e ->
    Pfedit.delete_current_proof ();
    msg (str "Could not prove noConfusion, this is a serious (unexpected) problem!");
    raise e

let no_confusion i =
  check_required_library ["Coq";"Logic";"JMeq"];
  let env = Global.env () in
  let istr = string_of_id i in
  try
    match Nametab.locate (qualid_of_string istr) with
    | IndRef ind ->
       let mind = lookup_mind_specif env ind in
            let no_conf = add_prefix "NoConfusion_" i in
            let little_no_conf = add_prefix "noConfusion_" i in
            (* msg (print_constr (construct_no_conf_body env ind mind)); TODO: Print a better message *)
            let _ = Declare.declare_constant no_conf (construct_no_conf_declaration env ind mind) in
            let no_conf_ty = Nametab.locate (qualid_of_string ("NoConfusion_"^istr)) in
            let env = Global.env () in
            Declare.declare_constant little_no_conf (construct_little_no_conf env ind mind little_no_conf no_conf_ty);
            ()
    | _ -> msg (str (istr^" is not an inductive."))
  with Not_found -> msg (str ("Inductive "^istr^" not found in global environment."))
 

VERNAC COMMAND EXTEND Derive_NoConfusion
| [ "Derive" "NoConfusion" ident(i) ] -> [ no_confusion i ]
END

% Unprogramming a permutation machine

stack([],[],[]) --> [].
stack([push|Instrs],[I|IS],SS) --> stack(Instrs,IS,[I|SS]).
stack([pop|Instrs],IS,[S|SS]) --> [S], stack(Instrs,IS,SS).

% ?- phrase(stack(Instructions, [1,2,3,4,5], []), [1,2,4,3,5], []).
% Instructions = [push, pop, push, pop, push, push, pop, pop, push, pop] .

Implementing tactics in Coq

Require Import List.

Section propr.
  Variable Sym : Set.
  Variable lookup : Sym -> Prop.
  Variable eq_Sym_dec : forall s s' : Sym, {s = s'} + {s <> s'}.
  
  Inductive prop : Set :=
  | var : Sym -> prop
  | imp : prop -> prop -> prop.
  
  Fixpoint interpret (p : prop) : Prop :=
    match p with
      | var i => lookup i
      | imp p q => interpret p -> interpret q
    end.
  
  Fixpoint assume (context : list Sym) :=
    match context with
      | nil => True
      | i :: is => lookup i /\ assume is
    end.
  
  Fixpoint contextLookup (i : Sym) (context : list Sym) :=
    match context as context' return option (assume context' -> interpret (var i)) with
      | nil => None
      | j::js =>
        match eq_Sym_dec i j with
          | left eql =>
            match eql with
              | refl_equal =>
                Some (fun hypotheses =>
                  match hypotheses with
                    | conj J _ => J
                  end)
            end
          | right _ =>
            match contextLookup i js with
              | Some Prf =>
                Some (fun hypotheses =>
                  match hypotheses with
                    | conj _ Js => Prf Js
                  end)
              | None => None
            end
        end
    end.
  
  Fixpoint proveable' (p : prop) (context : list Sym) : option (assume context -> interpret p) :=
    match p as p' return option (assume context -> interpret p') with
      | var i => contextLookup i context
      | imp (var i) q =>
        match proveable' q (i :: context) with
          | Some Hypo'X => Some (fun Hyp o => Hypo'X (conj o Hyp))
          | None => None
        end
      | imp _ x => None
    end.
  
  Definition some X (x : option X) :=
    match x with
      | Some _ => True
      | None => False
    end.
  Implicit Arguments some [X].
  
  Theorem proveable'_proveable p : some (proveable' p nil) -> interpret p.
    intro p; destruct (proveable' p nil); [ exact i | simpl; tauto ].
  Qed.

End propr.


Require Import Arith.

Theorem test (X Y Z W : Prop) : X -> Y -> Z -> X -> Y -> Z.
intros X Y Z W.
exact
  (proveable'_proveable
    nat
    (fun i =>
      match i with
        | 0 => X
        | 1 => Y
        | 2 => Z
        | 3 => W
        | _ => False
      end)
    eq_nat_dec
    (imp _ (var _ 0)
      (imp _ (var _ 1)
        (imp _ (var _ 2)
          (imp _ (var _ 0)
            (imp _ (var _ 1) (var _ 2))))))
  I).
Qed.

Print test.
(**************

test = 
fun X Y Z W : Prop =>
proveable'_proveable nat
  (fun i : nat =>
   match i with
   | 0 => X
   | 1 => Y
   | 2 => Z
   | 3 => W
   | S (S (S (S _))) => False
   end) eq_nat_dec
  (imp nat (var nat 0)
     (imp nat (var nat 1)
        (imp nat (var nat 2)
           (imp nat (var nat 0) (imp nat (var nat 1) (var nat 2)))))) I
     : forall X Y Z : Prop, Prop -> X -> Y -> Z -> X -> Y -> Z

 ***************)

eq_fin_dec via NoConfusion

Require Import JMeq.
Infix "==" := JMeq (at level 30).
Notation "X =/= Y" := (X == Y -> False) (at level 30).

Inductive Fin : nat -> Set :=
| fz n : Fin (S n)
| fs n : Fin n -> Fin (S n).

Fixpoint Fin_NoConfusion (P : Type) (n : nat) (f f' : Fin n) {struct f} :=
  match f, f' with
    | fz _, fz _ => P -> P
    | fs _ f, fs _ f' => (f == f' -> P) -> P
    | _, _ => P
  end.

Definition Fin_noConfusion P n (f f' : Fin n) : f == f' -> Fin_NoConfusion P n f f'.
intros P n f f' Eq.
elim Eq.
elim f;
  simpl; intros; tauto.
Defined.

Definition fs_injective (P : Type) (n : nat) (f f' : Fin n)
  : (f == f' -> P) -> (fs n f == fs n f' -> P)
  := fun m Eq =>
    Fin_noConfusion P (S n) (fs n f) (fs n f') Eq m.

Definition fz_fs_clash (P : Type) (n : nat) (f : Fin n)
  : fz n == fs n f -> P
  := fun Eq =>
    Fin_noConfusion P (S n) (fz n) (fs n f) Eq.

Definition eq_fin_dec n : forall f f' : Fin n, {f == f'} + {f =/= f'}.
refine (fix eq_fin_dec n (f f' : Fin n) {struct f'} : {f == f'} + {f =/= f'} :=
  match f in Fin n, f' in Fin n' return n = n' -> {f == f'} + {f =/= f'} with
    | fz _, fz _ => _
    | fs _ _, fz _ => _
    | fz _, fs _ _ => _
    | fs _ _, fs _ _ => _
  end (refl_equal _));
intro Eq; injection Eq; clear Eq; intro Eq.

left; rewrite Eq; reflexivity.

right; rewrite Eq; intro; exact (fz_fs_clash False _ _ H).

right; rewrite <- Eq; intro; exact (fz_fs_clash False _ _ (sym_JMeq H)).

clear f f' n; subst n0.
destruct (eq_fin_dec n1 f0 f1).
left; elim j; reflexivity.
right; intro; apply f; exact (fs_injective _ _ _ _ (fun Eq => Eq) H).
Defined.

A different approach

Just typing out stuff from http://www.cs.nott.ac.uk/~pwm/ .

module Universe where

open import Data.Nat

data SPT : ℕ -> Set1 where
 vz : {n : ℕ} -> SPT (suc n)
 vs : {n : ℕ} -> SPT n -> SPT (suc n)
 _[_] : {n : ℕ} -> SPT (suc n) -> SPT n -> SPT n
 “0” : {n : ℕ} -> SPT n
 “1” : {n : ℕ} -> SPT n
 _“+”_ : {n : ℕ} -> SPT n -> SPT n -> SPT n
 _“×”_ : {n : ℕ} -> SPT n -> SPT n -> SPT n
 _“->”_ : {n : ℕ} -> (K : Set) -> SPT n -> SPT n
 “μ”_ : {n : ℕ} -> SPT (suc n) -> SPT n

data Tel : ℕ -> (ℕ -> Set1) -> Set2 where
 ε : (F : ℕ -> Set1) -> Tel zero F
 _^_ : {F : ℕ -> Set1} -> {n : ℕ} -> F n -> Tel n F -> Tel (suc n) F

data ⟦_⟧_ : {n : ℕ} -> SPT n -> Tel n SPT -> Set2 where
 top : {n : ℕ} -> {T' : Tel n SPT} -> {T : SPT n} ->
   ⟦ T ⟧ T' -> ⟦ vz ⟧ (T ^ T')
 pop : {n : ℕ} -> {T' : Tel n SPT} -> {S T : SPT n} ->
   ⟦ T ⟧ T' -> ⟦ vs T ⟧ (S ^ T')
 def : {n : ℕ} -> {T' : Tel n SPT} -> {A : SPT n} -> {F : SPT (suc n)} ->
   ⟦ F ⟧ (A ^ T') -> ⟦  F [ A ]  ⟧ T'
 void : {n : ℕ} -> {T' : Tel n SPT} ->
   ⟦ “1” ⟧ T'
 inl : {n : ℕ} -> {T' : Tel n SPT} -> {S T : SPT n} ->
   ⟦ S ⟧ T' -> ⟦ S “+” T ⟧ T'
 inr : {n : ℕ} -> {T' : Tel n SPT} -> {S T : SPT n} ->
   ⟦ T ⟧ T' -> ⟦ S “+” T ⟧ T'
 pair : {n : ℕ} -> {T' : Tel n SPT} -> {S T : SPT n} ->
   ⟦ S ⟧ T' -> ⟦ T ⟧ T' -> ⟦ S “×” T ⟧ T'
 funk : {n : ℕ} -> {T' : Tel n SPT} -> {K : Set} -> {T : SPT n} ->
  (f : K -> ⟦ T ⟧ T') -> ⟦ (K “->” T) ⟧ T'
 miso : {n : ℕ} -> {T' : Tel n SPT} -> {F : SPT (suc n)} ->
   ⟦ F ⟧ ((“μ” F) ^ T') -> ⟦ (“μ” F) ⟧ T'



“Nat” : {n : ℕ} -> SPT n
“Nat” = “μ” (“1” “+” vz)

“zero” : {n : ℕ} -> {T' : Tel n SPT} -> ⟦ “Nat” ⟧ T'
“zero” = miso (inl (void))

“succ” : {n : ℕ} -> {T' : Tel n SPT} -> ⟦ “Nat” ⟧ T' -> ⟦ “Nat” ⟧ T'
“succ” x = miso (inr (top x))


data “Nat”-View : {n : ℕ} -> {T' : Tel n SPT} -> ⟦ “Nat” ⟧ T' -> Set2 where
 isZero : {n : ℕ} -> {T' : Tel n SPT} -> “Nat”-View {n} {T'} “zero”
 isSucc : {n : ℕ} -> {T' : Tel n SPT} -> (x : ⟦ “Nat” ⟧ T') -> “Nat”-View {n} {T'} (“succ” x)

viewNat : {n : ℕ} -> {T' : Tel n SPT} -> (n : ⟦ “Nat” ⟧ T') -> “Nat”-View n
viewNat {n} {T'} (miso Q) = aux1 Q
 where aux3 : (r : ⟦ vz ⟧ ((“μ” (“1” “+” vz)) ^ T')) -> “Nat”-View (miso (inr r))
       aux3 (top x) = isSucc x
       aux2 : (l : ⟦ “1” ⟧ ((“μ” (“1” “+” vz)) ^ T')) -> “Nat”-View (miso (inl l))
       aux2 void = isZero
       aux1 : (u : ⟦ “1” “+” vz ⟧ ((“μ” (“1” “+” vz)) ^ T')) -> “Nat”-View (miso u)
       aux1 (inl U) = aux2 U
       aux1 (inr V) = aux3 V

“add” : {n : ℕ} -> {T' : Tel n SPT} -> ⟦ “Nat” ⟧ T' -> ⟦ “Nat” ⟧ T' -> ⟦ “Nat” ⟧ T'
“add” x y with viewNat x
“add” (miso (inl (void))) y | isZero = y
“add” (miso (inr (top x))) y | isSucc .x = “succ” (“add” x y)


test = “add” {zero} {ε SPT}
         (“succ” (“succ” (“succ” “zero”)))
         (“succ” (“succ” “zero”))

{- =
miso
(inr
 (top
  (miso
   (inr
    (top
     (miso
      (inr
       (top
        (miso (inr (top (miso (inr (top (miso (inl void)))))))))))))))) -}

Emulate Agda style pattern matching in Coq using ideas frow Eliminating Dependent Pattern Matching..

Require Import JMeq.
Infix "==" := JMeq (at level 31).
Notation "[ x : X ]  == [ y : Y ]" := (@JMeq X x Y y) (at level 30).
Notation "X =/= Y" := (JMeq _ X _ Y -> False) (at level 30).


Derive NoConfusion nat.
Definition noConfusion_nat (P : Type) (u v : nat) : JMeq u v -> NoConfusion_nat P u v.
intros.
elim H.
elim u;
  simpl; intros; tauto.
Defined.


Inductive SPT : nat -> Type :=
| vz {n} : SPT (S n)
| vs {n} : SPT n -> SPT (S n)
| of {n} : SPT (S n) -> SPT n -> SPT n
| q_zero_q {n} : SPT n
| q_one_q {n} : SPT n
| q_sum_q {n} : SPT n -> SPT n -> SPT n
| q_mul_q {n} : SPT n -> SPT n -> SPT n
| q_arrow_q {n} : Type -> SPT n -> SPT n
| q_mu_q {n} : SPT (S n) -> SPT n.
Derive NoConfusion SPT.
Definition noConfusion_SPT (P : Type) (e1 : nat) (u v : SPT e1) : JMeq u v -> NoConfusion_SPT P e1 u v.
intros.
elim H.
elim u;
  simpl; intros; tauto.
Defined.



Inductive Tel : nat -> (nat -> Type) -> Type :=
| eps : forall {F}, Tel 0 F
| telCons : forall {F} {n}, Tel n F -> F n -> Tel (S n) F.
Infix ";" := telCons (at level 27, left associativity).
Derive NoConfusion Tel.
Definition noConfusion_Tel (P : Type) (e1 : nat) (e2 : nat -> Type) (u v : Tel e1 e2) : JMeq u v -> NoConfusion_Tel P e1 e2 u v.
intros.
elim H.
elim u;
  simpl; intros; tauto.
Defined.



Reserved Notation "⟦  type ⟧ scope" (at level 30, no associativity).
Inductive Interpretation : forall n, SPT n -> Tel n SPT -> Type :=
| top {n} {T' : Tel n SPT} {T : SPT n}
  : ⟦ T ⟧ T' -> ⟦ vz ⟧ (T';T)
| pop {n} {T' : Tel n SPT} {S T : SPT n}
  : ⟦ T ⟧ T' -> ⟦ vs T ⟧ (T';S)
| def {n} {T' : Tel n SPT} {A : SPT n} {F : SPT (S n)}
  : ⟦ F ⟧ (T'; A) -> ⟦ of F A ⟧ T'
| void {n} {T' : Tel n SPT}
  : ⟦ q_one_q ⟧ T'
| inl {n} {T' : Tel n SPT} {S T : SPT n}
  : ⟦ S ⟧ T' -> ⟦ q_sum_q S T ⟧ T'
| inr {n} {T' : Tel n SPT} {S T : SPT n}
  : ⟦ T ⟧ T' -> ⟦ q_sum_q S T ⟧ T'
| pair {n} {T' : Tel n SPT} {S T : SPT n}
  : ⟦ S ⟧ T' -> ⟦ T ⟧ T' -> ⟦ q_mul_q S T ⟧ T'
| funk {n} {T' : Tel n SPT} {K : Type} {T : SPT n}
  : (K -> ⟦ T ⟧ T') -> ⟦ q_arrow_q K T ⟧ T'
| miso {n} {T' : Tel n SPT} {F : SPT (S n)}
  : ⟦ F ⟧ (T';q_mu_q F) -> ⟦ q_mu_q F ⟧ T'
where "⟦  type ⟧ scope" := (Interpretation _ type scope).
Derive NoConfusion Interpretation.
Definition noConfusion_Interpretation (P : Type) (e1 : nat) (e2 : SPT e1) (e3 : Tel e1 SPT) (u v : ⟦e2 ⟧ e3) : JMeq u v -> NoConfusion_Interpretation P e1 e2 e3 u v.
intros.
elim H.
elim u;
  simpl; intros; tauto.
Defined.



Definition mu_injective (P : Type) (e1 : nat) (u v : SPT (S e1))
  : (e1 == e1 -> u == v -> P) -> (q_mu_q u == q_mu_q v -> P)
  := fun m Eq =>
    noConfusion_SPT P _ (q_mu_q u) (q_mu_q v) Eq m.

Definition mu_vz_clash (P : Type) (n : nat) (F : SPT (S (S n)))
  : q_mu_q F == vz -> P
  := fun Eq =>
    noConfusion_SPT P (S n) (q_mu_q F) vz Eq.



Definition q_Nat_q {n} : SPT n := q_mu_q (q_sum_q q_one_q vz).
Definition q_O_q {n} {T' : Tel n SPT} : ⟦ q_Nat_q ⟧ T' := miso (inl void).
Definition q_S_q {n} {T' : Tel n SPT} : ⟦ q_Nat_q ⟧ T' -> ⟦ q_Nat_q ⟧ T' := fun x => miso (inr (top x)).

Inductive q_Nat_q'View {n} {T' : Tel n SPT} : ⟦ q_Nat_q ⟧ T' -> Type :=
| isO : q_Nat_q'View q_O_q
| isS : forall x : ⟦ q_Nat_q ⟧ T', q_Nat_q'View (q_S_q x).



Ltac dpm_lift := repeat match goal with H : _ |- _ => intro Eq; revert H; revert Eq end.
Ltac dpm_prepare :=
  match goal with
    | |- @JMeq _ ?x _ ?x -> _ => intros _; dpm_prepare
    | |- @JMeq _ _ _ _ -> _ => dpm_lift
    | _ => intro; dpm_prepare
  end.

Ltac dpm_subst := intro Eql;
  match type of Eql with @JMeq _ ?x _ ?y =>
    (rewrite Eql; clear x Eql) || (rewrite <- Eql; clear y Eql)
  end.

Ltac dpm_confusion := intro Eql;
  match goal with |- ?P =>
    apply (noConfusion_nat P _ _ Eql)||
    apply (noConfusion_SPT P _ _ _ Eql)||
    apply (noConfusion_Tel P _ _ _ _ Eql)||
    apply (noConfusion_Interpretation P _ _ _ _ _ Eql)
  end.

Ltac dpm_specialize := repeat (dpm_prepare; (dpm_subst||dpm_confusion)).



Definition view'q_Nat_q
  (n : nat) (Ts : Tel n SPT) (x : ⟦ q_Nat_q ⟧ Ts) : (@q_Nat_q'View n Ts x).
intros.

refine
  (Interpretation_rect
    (fun n' S' Ts' x' =>
      n == n' -> @q_Nat_q n == S' -> Ts == Ts' -> x == x' ->
      q_Nat_q'View x)
    _ _ _ _ _ _ _ _ _
               n               q_Nat_q                Ts             x
    (JMeq_refl n) (JMeq_refl (@q_Nat_q n)) (JMeq_refl Ts) (JMeq_refl x));
unfold q_Nat_q in *;
dpm_specialize;
intros _.

refine
  (Interpretation_rect
    (fun n0' S' Ts' i' =>
      S n0 == n0' -> q_sum_q q_one_q vz == S' -> T'; q_mu_q (q_sum_q q_one_q vz) == Ts' -> i == i' ->
      q_Nat_q'View (miso i))
    _ _ _ _ _ _ _ _ _
    (S n0) (q_sum_q q_one_q vz) (T'; q_mu_q (q_sum_q q_one_q vz)) i
    (JMeq_refl (S n0)) (JMeq_refl (q_sum_q q_one_q vz)) (JMeq_refl (T'; q_mu_q (q_sum_q q_one_q vz))) (JMeq_refl i));
dpm_specialize;
intros _.

refine
  (Interpretation_rect
    (fun n0' S' Ts' i0' =>
      S n0 == n0' -> q_one_q == S' -> (T'; q_mu_q (q_sum_q q_one_q vz)) == Ts' -> i0 == i0' ->
      q_Nat_q'View (miso (inl i0)))
    _ _ _ _ _ _ _ _ _
    (S n0) q_one_q (T'; q_mu_q (q_sum_q q_one_q vz)) i0
    (JMeq_refl (S n0)) (JMeq_refl (q_one_q)) (JMeq_refl (T'; q_mu_q (q_sum_q q_one_q vz))) (JMeq_refl i0));
dpm_specialize.

exact isO.

refine
  (Interpretation_rect
    (fun n0' S' Ts' i0' =>
      S n0 == n0' -> vz == S' -> (T'; q_mu_q (q_sum_q q_one_q vz)) == Ts' -> i0 == i0' ->
      q_Nat_q'View (miso (inr i0)))
    _ _ _ _ _ _ _ _ _
    (S n0) vz (T'; q_mu_q (q_sum_q q_one_q vz)) i0
    (JMeq_refl (S n0)) (JMeq_refl vz) (JMeq_refl (T'; q_mu_q (q_sum_q q_one_q vz))) (JMeq_refl i0));
dpm_specialize;
intros _.

exact (isS i).

Defined.

Semigroup/Group proof

Definition associativity (T : Set) (o : T -> T -> T) :=
  forall x y z, (o (o x y) z) = (o x (o y z)).

Record Semigroup : Type := makeSemigroup {
  T : Set;
  o : T -> T -> T;
  assoc : associativity T o
}.

Record Group : Type := makeGroup {
  T' : Set;
  o' : T' -> T' -> T';
  assoc' : associativity T' o';
  I : T';
  unit' : forall u : T', exists v, o' u v = I
}.

(* Any semigroup S with a right unit, and right inverse forall a in
   S is a group *)

Theorem ex10
  (S : Semigroup)
  (right_unit : T S)
  (right_unit_meaning : forall a, (o S) a right_unit = a)
  (right_inverse : forall a, exists b, (o S) a b = right_unit)
: (* --------------------------------------------------------- *)
  exists I : T S,
    forall u : T S, exists v, (o S) u v = I.

intros.
exists right_unit.

intro.

destruct (right_inverse u).
exists x.

assumption.
Qed.