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"

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

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.

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.

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 closure

data Graph a = {- DeadEnd | -} a :-->: [Graph a] deriving Show

transitiveClosure location = location :-->: map transitiveClosure (flights location)

{-- define the truncation of any cyclical journeys

finite visited DeadEnd = DeadEnd
finite visited (location :-->: destinations)
 | already visited location = DeadEnd
 |         otherwise        = location :-->: map (finite (location : visited)) destinations

already = flip elem
-}

{-- remove any 'DeadEnd's left over

simplify DeadEnd = DeadEnd
simplify (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 visited

holidays = simplifyFinite [] . transitiveClosure


-- > holidays Paris
-- Paris :-->: [London :-->: [Shanghai :-->: [Tokyo :-->: [],
--                                            NewYork :-->: []],
--                            NewYork :-->: []]]
-- > holidays London 
-- London :-->: [Paris :-->: [],
--               Shanghai :-->: [Tokyo :-->: [Paris :-->: []],
--                               NewYork :-->: []],
--               NewYork :-->: []]

my thought process for breadth first numbering

data Tree a = Leaf a | Branch a (Tree a) (Tree a) deriving Show

i 0 = Leaf 0
i n = Branch 0 (i (n-1)) (i (n-1))


identity (Leaf i) = Leaf i
identity (Branch i left right) = Branch i (identity left) (identity right)


depth current (Leaf _) = Leaf current
depth current (Branch _ left right) = Branch current (depth (current + 1) left) (depth (current + 1) right)


depth' current (Leaf i) = Leaf i
depth' current (Branch i left right) = Branch i left' right'
 where left' = depth' (current + 1) left
       right' = depth' (current + 1) right


depth'' 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 right


depth''' 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' right

with = (,)


unfold step current = case step current of Nothing -> current ; Just next -> unfold step next


breadth 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)))

Type Error

Error:
In environment
ty : type
m : term ty
eq_term_dec :
forall (m' : {m' : term ty | size m' < size m}) (n : term ty),
{`m' = n} + {`m' <> n}
n : term ty
eq_term_dec0 :
forall (ty : type) (m n : term ty),
{[m : (term ty)]= [n : (term ty)]} + {m =/= n}
ty0 : type
m0 : term ty0
n0 : term ty0
uTy : type
vTy : type
u : term (uTy --> vTy)
v : term uTy
uTy' : type
vTy' : type
u' : 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_var
u0 : term (uTy --> vTy)
v0 : term uTy
u'0 : term (uTy --> vTy)
v'0 : term uTy
filtered_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}".

Variadic via GADT

data Pill a where
 Stop :: Pill Integer
 O :: Pill (Pill a -> a)

collect :: Integer -> Pill a -> a
collect i Stop = i
collect 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

Somewhat Pointfree Haskell Huffman Tree

{-# LANGUAGE NoMonomorphismRestriction #-}

import Prelude hiding (Either(..))
import Data.List

import Data.Maybe
import Data.Ord
import Control.Monad.Reader

lookdown :: (Eq b) => [(a, b)] -> b -> Maybe a

lookdown 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) Branch

depthFirstTraversal = foldHuff return (++)

-- foldHuff (!) (*) t =
--   (return T) ++

--       (return F) ++
--       (return T)
-- = [T,F,T]

member e = foldHuff (== e) (||)


data Direction = Left | Right deriving Show

type 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 . sort

joinTrees ((p1,t1) : (p2,t2) : freqs) = joinTrees (insertBy (comparing fst) (p1 + p2,Branch t1 t2) freqs)
joinTrees [(_,tree)] = tree

huffmanTree = joinTrees . frequencies

codeTable = depthFirstTraversal . label . huffmanTree

encode 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 path
traverse (Branch l r) (Right:path) = traverse r path
traverse _ [] = Nothing

huffmanDecode = 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 string
savings 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

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.