Friday 31 October 2008

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

Monday 27 October 2008


% 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] .

Sunday 12 October 2008

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

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

Saturday 11 October 2008

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.

Friday 10 October 2008

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.

Monday 6 October 2008

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.