## Friday, 26 December 2008

### Other Peoples Thoughts

"i kinda like haskell and erlang but i don't think they make it any easier to do anything. by the time you learn how to do the one liners, time has passed and you've become a professor of computer science, and your applications no longer matter."

"wow lisp occured in 1958"

"Yeah, but Haskell does such nice things for you. Like pattern matching? Very mathematical feel"

regarding C: "damn it.I m doing something so simple and its takes time.its like traveling from the UK to France via China"

## Sunday, 21 December 2008

### Common Subexpression Elimination

`;; My example of when mutation is a useful tool that simplifies things.(define (identity i) i)(define (concat xs) (apply append xs))(define (concat-map f x) (concat (map f x)))(define (sort by xs)  (define (insert by x xs)    (if (null? xs)        (list x)        (if (< (by x) (by (car xs)))            (cons x xs)            (cons (car xs) (insert by x (cdr xs))))))  (if (null? xs) '()      (insert by (car xs) (sort by (cdr xs)))));; <variadic-tree> ::= <leaf> | (<variadic-tree> ...);; <leaf> is any non-list datum(define (leaf? datum) (not (list? datum)))(define (variadic-tree leaf nodes)  (lambda (tree)    (if (leaf? tree)        (leaf tree)        (apply nodes (map (variadic-tree leaf nodes) tree)))))(define copy-tree (variadic-tree identity list))(define exp-1  (copy-tree   '(+ (* (- x-1 x-2) (- x-1 x-2))       (* (- y-1 y-2) (- y-1 y-2))       (* (- z-1 z-2) (- z-1 z-2)))))(define (splat tree)  (if (leaf? tree)      '()      (cons tree (concat-map splat tree))))(define (subexpressions tree) (sort length (cdr (splat tree))))(define (eliminate exp sub sym)  (cond ((null? exp) exp)        ((leaf? exp) exp)        ((cond ((equal? sub (car exp)) (set-car! exp sym))               (else (eliminate (car exp) sub sym)))         (eliminate (cdr exp) sub sym)         exp)))(define gensym  (let ((n 0))    (lambda ()      (set! n (+ n 1))      (string->symbol (string-append "g" (number->string n))))))(define (eliminate-subexpressions env exp subs)  (cond ((null? subs) `(let ,(reverse env) ,exp))        (else         (let* ((g (gensym))                (sub (car subs))                (exp-2 (eliminate exp sub g)))           (eliminate-subexpressions (cons (list g sub) env) exp-2 (subexpressions exp-2))))));; (eliminate-subexpressions '() exp-1 (subexpressions exp-1));; =>;; (let ((g1 (- z-1 z-2));;       (g2 (* g1 g1));;       (g3 (- y-1 y-2));;       (g4 (* g3 g3));;       (g5 (- x-1 x-2));;       (g6 (* g5 g5)));;   (+ g6 g4 g2))`

## Monday, 8 December 2008

### Virgin Killer

http://www.theregister.co.uk/2008/12/07/brit_isps_censor_wikipedia/

http://iwfwebfilter.thus.net/error/blocked.html

You are currently unable to edit pages on Wikipedia.

You can still read pages, but cannot edit, change, or create them.

Editing from 193.195.3.41 (your account, IP address, or IP address range) has been disabled by Lucasbfr for the following reason(s):

193.195.3.41 <-- This is the IP of the filter which I view wikipedia through.

I am not able to edit wikipedia because one of the million people viewing it through the same ip filter as me vandalised as article and was banned. I found out this censorship was the reason. Maybe if you want to help abused children you could find a way that doesn't mean sitting in a comfy chair fiddling with 1's and 0's and patting yourself on the back.

Statement by "IWF":

"IWF statement regarding Wikipedia URL
IWF is the UK’s internet ‘Hotline’ for the public and IT professionals to report potentially illegal online content within our remit. We work in partnership with the online industry, law enforcement, government, the education sector, charities, international partners and the public to minimise the availability of this content, specifically, child sexual abuse content hosted anywhere in the world and criminally obscene and incitement to racial hatred content hosted in the UK. We are an independent self-regulatory body, funded by the EU and the wider online industry, including internet service providers, mobile operators and manufacturers, content service providers, filtering companies, search providers, trade associations and the financial sector as well as other organisations that support us for corporate social responsibility reasons.

We help internet service providers and hosting companies to combat abuse of their networks through our national ‘notice and take-down’ service which alerts them to potentially illegal content within our remit on their systems and we provide unique data to law enforcement partners in the UK and abroad to assist investigations into the distributers of potentially illegal online content. As sexually abusive images of children are primarily hosted abroad, we facilitate the industry-led initiative to protect users from inadvertent exposure to this content by blocking access to it through our provision of a dynamic list of child sexual abuse URLs.

A Wikipedia web page, was reported through the IWF’s online reporting mechanism in December 2008. As with all child sexual abuse reports received by our Hotline analysts, the image was assessed according to the UK Sentencing Guidelines Council (page 109). The content was considered to be a potentially illegal indecent image of a child under the age of 18, but hosted outside the UK. The IWF does not issue takedown notices to ISPs or hosting companies outside the UK, but we did advise one of our partner Hotlines abroad and our law enforcement partner agency of our assessment. The specific URL (individual webpage) was then added to the list provided to ISPs and other companies in the online sector to protect their customers from inadvertent exposure to a potentially illegal indecent image of a child."

I had not realized that wikipedia (The free encylcopedia) is a hive of child sexual abuse and a den for pedophiles.

to IWF: Wikipedia is a website for people that are like to read and learn things, studying, or writing. You are not helping the world or sexually abused children by censoring it. Realize you have become robots and by following your protocols you're actually worsening the planet for everyone.

This is how all Authoritarian/Stalinist governments work.
First they choose to censor something that most people would find reasonable to censor, such as the image of a naked child.
Before you know it, all wikipedia pages relating to opposition politicians and opposition parties will also be unavailable.
I see IWF are 'supported' by both the Home Office and the Dept of Business, Enterprise and Regulatory Reform, enough said !

For people like Berlusconi the world will always be open and free. He can get on a jet and talk to his friends in Australia in person. For the rest of us, the internet will be what Berlusconi and his ilk allow us to have and see. And yes this is a small step, but there have been hundreds of little steps that add up.

## Tuesday, 2 December 2008

### Axiom Free NoConfusion in Coq

`Require Import Cast.Require Import Fin.Ltac prove_noConfusion :=  intros;    match goal with Eql : ?x = _ |- _ =>      elim Eql; elim x; simpl; tauto end.(*Inductive nat : Set :=| O : nat| S : nat -> nat.*)Definition NoConfusion_nat (P : Type) (x y : nat) : Type :=  match x, y with    | O, O => P -> P    | O, S y => P    | S x, O => P    | S x, S y => (x = y -> P) -> P  end.Definition noConfusion_nat (P : Type) (x y : nat) :  x = y -> NoConfusion_nat P x y.prove_noConfusion.Defined.Definition eq_nat_dec : forall x y : nat, {x = y} + {x <> y}.decide equality.Defined.Definition eq_nat_dec' : forall x y : nat, x = y \/ x <> y.decide equality.Defined.(*Inductive Fin : nat -> Set :=| fz : forall n, Fin (S n)| fs : forall n, Fin n -> Fin (S n).*)Notation FinINeq f g := (INeq nat Fin _ f _ g).Definition NoConfusion_Fin (P : Type) (i : nat) (x y : Fin i) : Type :=  match x, y with    | fz _, fz _ => P -> P    | fz _, fs _ _ => P    | fs _ _, fz _=> P    | fs x_i x, fs y_i y => (FinINeq x y -> P) -> P  end.Definition noConfusion_Fin (P : Type) (i : nat) (x y : Fin i) :  x = y -> NoConfusion_Fin P i x y.prove_noConfusion.Defined.Definition fz_fs_clash (P : Type) (n : nat) (f : Fin n)  : fz = fs f -> P  := fun Eq =>    noConfusion_Fin P (S n) (fz) (fs f) Eq.Definition fs_inj {n} {f f' : Fin n}  : fs f = fs f' -> f = f'  := fun Eq =>    noConfusion_Fin (f = f') _ _ _ Eq (INeq_eq nat Fin eq_nat_dec _ _ _).Inductive type : Set :=| Nat : type| Arrow : type -> type -> type.Definition eq_type_dec (s t : type) : { s = t } + { s <> t }.decide equality.Defined.Section equand.Variable vars : nat.Inductive equand : type -> Set :=| Zero : equand Nat| Succ : equand (Arrow Nat Nat)| VAR (V : Fin vars) : equand Nat| APP {A B} : equand (Arrow A B) -> equand A -> equand B.Notation equandINeq f g := (INeq type equand _ f _ g).Definition NoConfusion_equand (P : Type) (i : type) (x y : equand i) : Type :=  match x, y with    | Zero, Zero => P -> P    | Succ, Succ => P -> P    | VAR f, VAR f' => (f = f' -> P) -> P    | APP xi xj xf xo, APP yi yj yf yo =>      (equandINeq xf yf -> equandINeq xo yo -> P) -> P    | _, _ => P  end.Definition noConfusion_equand (P : Type) (i : type) (x y : equand i) : x = y -> NoConfusion_equand P i x y.prove_noConfusion.Defined.Definition Zero_One_clash (P : Type) (i : type)  : Zero = APP Succ Zero -> P  := fun Eq =>    noConfusion_equand P Nat Zero (APP Succ Zero) Eq.Definition APP_f_inj (u v : type) (F F' : equand (Arrow u v)) (O O' : equand u)  : @APP u v F O = @APP u v F' O' -> F = F'  := fun Eq =>    noConfusion_equand (F = F') _ _ _ Eq    (fun FEq OEq => INeq_eq _ _ eq_type_dec _ _ _ FEq).Definition APP_o_inj (u v : type) (F F' : equand (Arrow u v)) (O O' : equand u)  : @APP u v F O = @APP u v F' O' -> O = O'  := fun Eq =>    noConfusion_equand (O = O') _ _ _ Eq    (fun FEq OEq => INeq_eq _ _ eq_type_dec _ _ _ OEq).Definition eq_equand_dec : forall (t : type)(u v : equand t), {u = v} + {u <> v}.apply INeq_dec_dec.apply eq_type_dec.refine (fix eq_equand_dec (i : type) (I : equand i)                          (i' : type) (I' : equand i') {struct I} :                          {@INeq _ _ i I i' I'} + {~ @INeq _ _ i I i' I'} := _).refine (match I as I in equand i, I' as I' in equand i'        return {@INeq _ _ i I i' I'} + {~ @INeq _ _ i I i' I'}        with          | Zero, Zero => _          | Zero, Succ => _          | Zero, VAR _ => _          | Zero, APP _ _ _ _ => _          | Succ, Zero => _          | Succ, Succ => _          | Succ, VAR _ => _          | Succ, APP _ _ _ _ => _          | VAR _, Zero => _          | VAR _, Succ => _          | VAR _, VAR _ => _          | VAR _, APP _ _ _ _ => _          | APP _ _ _ _, Zero => _          | APP _ _ _ _, Succ => _          | APP _ _ _ _, VAR _ => _          | APP _ _ _ _, APP _ _ _ _ => _        end);try solve [ discriminate          | left; reflexivity          | right; intro Q; inversion Q          | destruct B; right; intro Q; inversion Q; discriminate          ].destruct (fin_eq_dec V V0); subst.left; reflexivity.right; intro Q; inversion Q; contradiction.destruct (eq_type_dec B B0);(destruct (eq_equand_dec _ e0 _ e2) as [Q|N];[inversion Q|idtac]);(destruct (eq_equand_dec _ e _ e1) as [Q'|N'];[inversion Q'|idtac]);  subst;try solve [ left;  rewrite Q; try apply eq_type_dec;  rewrite Q'; try apply eq_type_dec;    reflexivity ];right; intro NQ;  try inversion NQ;  try inversion Q;  try inversion Q';  try contradiction;  try subst;  try pose (APP_f_inj _ _ _ _ _ _ (INeq_eq _ _ eq_type_dec _ _ _ NQ));  try pose (APP_o_inj _ _ _ _ _ _ (INeq_eq _ _ eq_type_dec _ _ _ NQ)).apply N'; rewrite e3; reflexivity.apply N; rewrite e4; reflexivity.apply N; rewrite e4; reflexivity.Defined.Eval compute in (eq_equand_dec _  (APP Succ (APP Succ Zero))  (APP Succ (APP Succ Zero))).End equand.Print Assumptions eq_equand_dec.(* *  = left (APP Succ (APP Succ Zero) = APP Succ (APP Succ Zero) -> False) *      (refl_equal (APP Succ (APP Succ Zero))) *  : {APP Succ (APP Succ Zero) = APP Succ (APP Succ Zero)} + *    {APP Succ (APP Succ Zero) <> APP Succ (APP Succ Zero)} * * Computed fully, no JMeq_eq axiom stopping reduction * *)Require Import Coven.Require Import Arith.Require Import Omega.Print le.Lemma le_irrelevent : forall n m (H1 H2:le n m), H1=H2.refine (fix le_irrelevent n m (H1 H2:le n m) {struct H1} : H1=H2 := _).apply INeq_eq; auto with arith.refine (  match H1 as H1' in _ <= m', H2 as H2' in _ <= m''  return m = m' ->         m = m'' ->         INeq nat (le n) m H1 m' H1' ->         INeq nat (le n) m H2 m'' H2' ->         INeq nat (le n) m H1 m H2  with    | le_n, le_n => fun m'eq m''eq H1eq H2eq => _    | le_n, le_S p_m p_le => fun m'eq m''eq H1eq H2eq => !    | le_S p_m p_le, le_n => fun m'eq m''eq H1eq H2eq => !    | le_S p_m p_le, le_S p_m' p_le' => fun m'eq m''eq H1eq H2eq => _  end  (refl_equal _)  (refl_equal _)  (INeq_refl _ _ _ _)  (INeq_refl _ _ _ _)); subst; subst.rewrite (INeq_eq _ _ eq_nat_dec _ _ _ H1eq).rewrite (INeq_eq _ _ eq_nat_dec _ _ _ H2eq).reflexivity.omega.omega.injection m''eq; intro; subst.rewrite (INeq_eq _ _ eq_nat_dec _ _ _ H1eq).rewrite (INeq_eq _ _ eq_nat_dec _ _ _ H2eq).rewrite (le_irrelevent _ _ p_le p_le').reflexivity.Qed.Print Assumptions le_irrelevent.(** Closed under the global context **)`

### Dependently typed Data.Dynamic

`Require Import Eqdep_dec_defined.Section Cast.    Variable U:Type.  Variable F : U -> Type.    Variable eq_dec : forall x y:U, {x = y} + {x <> y}.    Definition eq_decide : forall x y:U, x = y \/ x <> y.  intros x y; destruct (eq_dec x y); [ left | right ]; assumption.  Defined.    Definition cast (i j : U) : F j -> option (F i) :=    fun J =>      match eq_dec j i with        | left Eql => match Eql in _ = i return option (F i) with                        | refl_equal => Some J                      end        | right _ => None      end.    Theorem cast_reflexivity (i : U) (I : F i) : cast i i I = Some I.    unfold cast; intro i; destruct (eq_dec i i);      [ subst | absurd (i = i); tauto ].    rewrite (eq_proofs_unicity eq_decide e (refl_equal i)).    reflexivity.  Defined.    Definition cast_injective (i : U) (I I' : F i) :    cast i i I = cast i i I' -> I = I'.  intros i I I'; repeat rewrite cast_reflexivity.  intro SomeEq; injection SomeEq; tauto.  Defined.    Inductive INeq (i : U)(I : F i) : forall (j : U)(J : F j), Prop :=  | INeq_refl : INeq i I i I.  Implicit Arguments INeq [i j].    Hint Resolve INeq_refl.    Definition INeq_eq (i : U)(I I' : F i) : INeq I I' -> I = I'.  intros i I I' inEq; apply cast_injective.  change ((fun i' I' => cast i i I = cast i i' I') i I').  elim inEq; reflexivity.  Defined.  Implicit Arguments INeq_eq [i I I'].    Lemma INeq_ind_r :    forall (i:U) (I J:F i) (P:F i -> Prop), P J -> INeq I J -> P I.    intros i I J P H Eql; rewrite (INeq_eq Eql); assumption.  Defined.    Lemma INeq_rec_r :    forall (i:U) (I J:F i) (P:F i -> Set), P J -> INeq I J -> P I.    intros i I J P H Eql; rewrite (INeq_eq Eql); assumption.  Defined.    Lemma INeq_rect_r :    forall (i:U) (I J:F i) (P:F i -> Type), P J -> INeq I J -> P I.    intros i I J P H Eql; rewrite (INeq_eq Eql); assumption.  Defined.    Definition INeq_dec_dec :    (forall (i:U)(I:F i) (j:U)(J:F j), {INeq I J} + {~INeq I J}) ->    (forall (i:U)(I J:F i), {I = J} + {I <> J}).  intros ineq_dec i I J; destruct (ineq_dec i I i J); [ left | right ].  apply INeq_eq; assumption.  contradict n; subst; reflexivity.  Defined.  End Cast.`

## Sunday, 30 November 2008

### Decidable Equality and Type Equality

`Require Import Eqdep_dec_defined.(** Same as Eqdep_dec but s/Qed/Defined/ **)Theorem dep_destruct :  forall (T : Type) (T' : T -> Type) x (v : T' x) (P : T' x -> Type),    (forall x' (v' : T' x') (Heq : x' = x),      P (match Heq in (_ = x) return (T' x) with           | refl_equal => v'         end)) ->      P v.  intros T T' x v P I; apply (I _ v (refl_equal _)).Defined.(** Stolen from http://www.cs.harvard.edu/~adamc/cpdt/ **)Inductive type : Set :=| Nat : type| Arrow : type -> type -> type.Definition eq_type_dec' (s t : type) : s = t \/ s <> t.decide equality.Defined.Inductive equand : type -> Set :=| Zero : equand Nat| Succ : equand (Arrow Nat Nat).Definition eq_equand_dec {T} (x y : equand T) : {x = y} + {x <> y}.intro.destruct x;  intro y; apply (dep_destruct type equand _ y);    intros T y' Teq; destruct y';      discriminate ||        rewrite <- (eq_proofs_unicity eq_type_dec' (refl_equal _) Teq).left; reflexivity.left; reflexivity.Defined.`

### Calculating Journeys

`-- WARNING: contains recursive programming-- For example data, pick some imaginary flight network:data Node = Paris | London | Shanghai | NewYork | Tokyo deriving (Eq, Show)flights Paris = [London]flights London = [Paris,Shanghai,NewYork]flights Shanghai = [Tokyo,NewYork]flights NewYork = [London]flights Tokyo = [Paris,London,Shanghai]-- and a convenient data representation of the transitive closuredata Graph a = {- DeadEnd | -} a :-->: [Graph a] deriving ShowtransitiveClosure location = location :-->: map transitiveClosure (flights location){-- define the truncation of any cyclical journeysfinite visited DeadEnd = DeadEndfinite visited (location :-->: destinations) | already visited location = DeadEnd |         otherwise        = location :-->: map (finite (location : visited)) destinationsalready = flip elem-}{-- remove any 'DeadEnd's left oversimplify DeadEnd = DeadEndsimplify (location :-->: destinations) = location :-->: purge (map simplify destinations)purge = foldr cons [] where cons DeadEnd ys = ys       cons x       ys = x : ys-}-- holidays = simplify . finite [] . transitiveClosure-- but fusing the truncation and simplification into one allows the 'DeadEnd' construtor to be erased!simplifyFinite visited (location :-->: destinations) = location :-->: filter (not . already visited) (map (simplifyFinite (location : visited)) destinations)already visited (location :-->: _) = elem location visitedholidays = simplifyFinite [] . transitiveClosure-- > holidays Paris-- Paris :-->: [London :-->: [Shanghai :-->: [Tokyo :-->: [],--                                            NewYork :-->: []],--                            NewYork :-->: []]]-- > holidays London -- London :-->: [Paris :-->: [],--               Shanghai :-->: [Tokyo :-->: [Paris :-->: []],--                               NewYork :-->: []],--               NewYork :-->: []]`

## Saturday, 22 November 2008

### my thought process for breadth first numbering

`data Tree a = Leaf a | Branch a (Tree a) (Tree a) deriving Showi 0 = Leaf 0i n = Branch 0 (i (n-1)) (i (n-1))identity (Leaf i) = Leaf iidentity (Branch i left right) = Branch i (identity left) (identity right)depth current (Leaf _) = Leaf currentdepth current (Branch _ left right) = Branch current (depth (current + 1) left) (depth (current + 1) right)depth' current (Leaf i) = Leaf idepth' current (Branch i left right) = Branch i left' right' where left' = depth' (current + 1) left       right' = depth' (current + 1) rightdepth'' current target (Leaf i) = Leaf (if current == target then i+1 else i)depth'' current target (Branch i left right) = Branch (if current == target then i+1 else i) left' right' where left' = depth'' (current + 1) target left       right' = depth'' (current + 1) target rightdepth''' current target delta (Leaf i) = Leaf (if current == target then i+delta else i) `with` (if current == target then delta+1 else delta)depth''' current target delta (Branch i left right) = Branch (if current == target then i+delta else i) left' right' `with` delta'' where (left',delta') = depth''' (current + 1) target (if current == target then delta+1 else delta) left       (right',delta'') = depth''' (current + 1) target delta' rightwith = (,)unfold step current = case step current of Nothing -> current ; Just next -> unfold step nextbreadth tree = case unfold step (0,0,tree) of (_,_,tree) -> tree where step (depth, delta, tree) = case depth''' 0 depth delta tree of         (tree, delta') -> if delta == delta' then Nothing else Just (depth + 1, delta', tree)-- > breadth (i 3)-- Branch 0 (Branch 1 (Branch 3 (Leaf 7)--                              (Leaf 8))--                    (Branch 4 (Leaf 9)--                              (Leaf 10)))--          (Branch 2 (Branch 5 (Leaf 11)--                              (Leaf 12))--                    (Branch 6 (Leaf 13)--                              (Leaf 14)))`

## Thursday, 20 November 2008

### Type Error

`Error:In environmentty : typem : term tyeq_term_dec :forall (m' : {m' : term ty | size m' < size m}) (n : term ty),{`m' = n} + {`m' <> n}n : term tyeq_term_dec0 :forall (ty : type) (m n : term ty),{[m : (term ty)]= [n : (term ty)]} + {m =/= n}ty0 : typem0 : term ty0n0 : term ty0uTy : typevTy : typeu : term (uTy --> vTy)v : term uTyuTy' : typevTy' : typeu' : term (uTy' --> vTy')v' : term uTy'vTyEq : vTy = vTy'filtered_var := eq_type_dec uTy uTy' : {uTy = uTy'} + {uTy <> uTy'}uTyEq : uTy = uTy'Heq_anonymous : in_left = filtered_varu0 : term (uTy --> vTy)v0 : term uTyu'0 : term (uTy --> vTy)v'0 : term uTyfiltered_var0 := eq_term_dec0 (uTy --> vTy) u0 u'0 :{[u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))]} + {u0 =/= u'0}filtered_var1 := eq_term_dec0 uTy v0 v'0 :{[v0 : (term uTy)]= [v'0 : (term uTy)]} + {v0 =/= v'0}branch_0 :=fun (wildcard' : [u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))])  (wildcard'0 : [u'0 : (term vTy)]= [filtered_var0 : (term vTy)])  (Heq_anonymous0 : in_left = filtered_var0)  (Heq_anonymous1 : in_left = filtered_var1) => in_left :forall  (wildcard' : [u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))])  (wildcard'0 : [u'0 : (term vTy)]= [filtered_var0 : (term vTy)]),in_left = filtered_var0 ->in_left = filtered_var1 ->{[app u0 v0 : (term vTy)]= [app u'0 v'0 : (term vTy)]} +{app u0 v0 =/= app u'0 v'0}branch_1 :=fun  (wildcard' : {[u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))]} +               {u0 =/= u'0})  (wildcard'0 : {[u'0 : (term vTy)]= [filtered_var0 : (term vTy)]} +                {u'0 =/= filtered_var0})  (H : forall         (wildcard'1 : [u0 : (term (uTy --> vTy))]= [u'0                       : (term (uTy --> vTy))])         (wildcard'2 : [u'0 : (term vTy)]= [filtered_var0 : (term vTy)]),       ~ (in_left = wildcard' /\ in_left = wildcard'0))  (Heq_anonymous0 : wildcard' = filtered_var0)  (Heq_anonymous1 : wildcard'0 = filtered_var1) => in_right :forall  (wildcard' : {[u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))]} +               {u0 =/= u'0})  (wildcard'0 : {[u'0 : (term vTy)]= [filtered_var0 : (term vTy)]} +                {u'0 =/= filtered_var0}),(forall   (wildcard'1 : [u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))])   (wildcard'2 : [u'0 : (term vTy)]= [filtered_var0 : (term vTy)]), ~ (in_left = wildcard' /\ in_left = wildcard'0)) ->wildcard' = filtered_var0 ->wildcard'0 = filtered_var1 ->{[app u0 v0 : (term vTy)]= [app u'0 v'0 : (term vTy)]} +{app u0 v0 =/= app u'0 v'0}Anonymous : [u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))]wildcard' := in_left :{[u0 : (term (uTy --> vTy))]= [u'0 : (term (uTy --> vTy))]} + {u0 =/= u'0}Anonymous0 : u'0 =/= wildcard'wildcard'0 := in_right :{[u'0 : (term vTy)]= [wildcard' : (term vTy)]} + {u'0 =/= wildcard'}The term "wildcard'0" has type "{[u'0 : (term vTy)]= [wildcard' : (term vTy)]} + {u'0 =/= wildcard'}" while it is expected to have type "{[u'0 : (term vTy)]= [filtered_var0 : (term vTy)]} +  {u'0 =/= filtered_var0}".`

## Saturday, 15 November 2008

`data Pill a where Stop :: Pill Integer O :: Pill (Pill a -> a)collect :: Integer -> Pill a -> acollect i Stop = icollect i O = collect (i+1)start = collect 0-- > start Stop-- 0-- > start O Stop-- 1-- > start O O Stop-- 2-- > start O O O Stop-- 3-- > start O O O O Stop-- 4-- > start O O O O O Stop-- 5`

## Sunday, 9 November 2008

### Somewhat Pointfree Haskell Huffman Tree

`{-# LANGUAGE NoMonomorphismRestriction #-}import Prelude hiding (Either(..))import Data.Listimport Data.Maybeimport Data.Ordimport Control.Monad.Readerlookdown :: (Eq b) => [(a, b)] -> b -> Maybe alookdown pairs i = lookup i (map swap pairs)onFst f (x,y) = (f x, y)swap (x,y) = (y,x)f & g = \x -> (f x, g x)infix 4 &-------data Huff a = Leaf a | Branch (Huff a) (Huff a) deriving Show-- -- Example tree:-- let t =--   (Branch (Leaf T)--           (Branch (Leaf F)--                   (Leaf T)))foldHuff leaf branch = φ where φ (Leaf o) = leaf o       φ (Branch left right) = branch (φ left) (φ right)-- foldHuff (!) (*) t =--   (* (! T)--      (* (! F)--         (! T)))instance Functor Huff where fmap f = foldHuff (Leaf . f) BranchdepthFirstTraversal = foldHuff return (++)-- foldHuff (!) (*) t =--   (return T) ++--       (return F) ++--       (return T)-- = [T,F,T]member e = foldHuff (== e) (||)data Direction = Left | Right deriving Showtype Path = [Direction]branch join left right = \φleft φright -> join (left φleft) (right φright)label = foldHuff (Leaf . (,) []) -- you are here                 (branch Branch (fmap (onFst (Left:))) -- first on your left                                (fmap (onFst (Right:))))type Freq a = (Integer, Huff a)frequencies = map (length & Leaf . head) . sortBy (comparing length) . group . sortjoinTrees ((p1,t1) : (p2,t2) : freqs) = joinTrees (insertBy (comparing fst) (p1 + p2,Branch t1 t2) freqs)joinTrees [(_,tree)] = treehuffmanTree = joinTrees . frequenciescodeTable = depthFirstTraversal . label . huffmanTreeencode codeTable = catMaybes . map (lookdown codeTable)huffmanCode = concat . join (encode . codeTable)traverse (Leaf o) path = Just (o, path)traverse (Branch l r) (Left:path) = traverse l pathtraverse (Branch l r) (Right:path) = traverse r pathtraverse _ [] = NothinghuffmanDecode = unfoldr . traverse-- forall text, length text > 1 ->correct text = huffmanDecode (huffmanTree text) (huffmanCode text) == text-- checking how many bits saved on an 8 bit encoded stringsavings text = length text * 8 - length (huffmanCode text)-- > huffmanTree "quick brown fox jumped over the lazy dog"-- Branch (Branch (Branch (Branch (Branch (Leaf 'i') (Leaf 'j')) (Branch (Leaf 'g') (Leaf 'h'))) (Branch (Branch (Leaf 'm') (Leaf 'n')) (Branch (Leaf 'k') (Leaf 'l')))) (Branch (Branch (Leaf 'd') (Leaf 'r')) (Branch (Branch (Leaf 'c') (Leaf 'f')) (Branch (Leaf 'a') (Leaf 'b'))))) (Branch (Branch (Leaf 'o') (Branch (Leaf 'u') (Leaf 'e'))) (Branch (Leaf ' ') (Branch (Branch (Branch (Leaf 't') (Leaf 'v')) (Branch (Leaf 'p') (Leaf 'q'))) (Branch (Branch (Leaf 'y') (Leaf 'z')) (Branch (Leaf 'w') (Leaf 'x'))))))-- > correct "quick brown fox jumped over the lazy dog"-- True-- > savings  "quick brown fox jumped over the lazy dog"-- 143`

## 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 Univopen Inductiveopen Utilopen Coqliblet 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 Definitionlet 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 elet 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 machinestack([],[],[]) --> [].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 whereopen import Data.Natdata 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 ndata Tel : ℕ -> (ℕ -> Set1) -> Set2 where ε : (F : ℕ -> Set1) -> Tel zero F _^_ : {F : ℕ -> Set1} -> {n : ℕ} -> F n -> Tel n F -> Tel (suc n) Fdata ⟦_⟧_ : {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 nviewNat {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.`