Fin is injective

Inductive Fin : nat -> Set :=
| fz : forall n, Fin (S n)
| fs : forall n, Fin n -> Fin (S n).
Implicit Arguments fz [n].
Implicit Arguments fs [n].
(* Fin is the family of finite types
 * Fin n is the type with 'n' distinct elements
 * Fin 0 ~ void
 * Fin 1 ~ unit
 * Fin 2 ~ bool
 *)

Inductive sumdys (A:Prop) (B:Type) : Type :=
| dyleft : A -> sumdys A B
| dyright : B -> sumdys A B.
(* Just because I prefer the Prop case to come first *)

Definition fz_or_fs n (f : Fin (S n)) : sumdys (f = fz) { f' | f = fs f' }.
intros; set (P n :=
  match n return Fin n -> Set with
    | O => fun _ => unit
    | S n => fun f => sumdys (f = fz) { f' | f = fs f' }
  end).

change (P (S n) f);
  destruct f;
    [ left; reflexivity |
      right; exists f; reflexivity ].
Defined.
Implicit Arguments fz_or_fs [n].

Lemma no_fin0 : Fin 0 -> forall P, P.
  intros f; refine
    match f in Fin n' return
      match n' with
        | O => forall P, P
        | S _ => True
      end
      with
      | fz _ => I
      | fs _ _ => I
    end.
Qed.

(* Destruct a fin down one level *)
Ltac fin_case f :=
  destruct (fz_or_fs f);
    match goal with
      | eq : f = fz |- _ =>
        try (rewrite eq in *; clear eq)
      | Ex : { f' | f = fs f' } |- _ =>
        destruct Ex;
          match goal with
            | eq : f = fs ?f' |- _ =>
              try (rewrite eq in *; clear eq)
          end end.

(* Smash a Fin to bits *)
Ltac destruct_fin f :=
  destruct (fz_or_fs f);
    match goal with
      | eq : f = fz |- _ =>
        try (rewrite eq in *; clear eq)
      | Ex : { f' | f = fs f' } |- _ =>
        destruct Ex;
          match goal with
            | eq : f = fs ?f' |- _ =>
              try (rewrite eq in *; clear eq);
                match type of f' with
                  | Fin 0 => apply (no_fin0 f')
                  | Fin (S _) => destruct_fin f'
                end end end.

Lemma one_fin1 : forall f : Fin 1, f = fz.
  intro f; destruct_fin f; reflexivity.
Qed.

Lemma two_fin2 : forall f : Fin 2, f = fz \/ f = fs fz.
  intro f; destruct_fin f; auto.
Qed.

Definition squish n : Fin (S (S n)) -> Fin (S n) :=
  fun f => match fz_or_fs f with
             | dyleft _ => fz
             | dyright (exist f _) => f
           end.
Implicit Arguments squish [n].
(* squish pushes down on the Fin *)

Fixpoint bump n (f : Fin n) : Fin (S n) :=
  match f with
    | fz _ => fz
    | fs _ f => fs (bump _ f)
  end.
Implicit Arguments bump [n].
(* bump lifts the family a Fin resides in *)

Fixpoint scum n : Fin (S n) :=
  match n with
    | O => fz
    | S n => fs (scum n)
  end.
Implicit Arguments scum [n].
(* scum always floats at the top *)


Lemma fs_injective n (x y : Fin n) : fs x = fs y -> x = y.
  intros; destruct n.
  apply (no_fin0 x).
  change (squish (fs x) = squish (fs y)); congruence.
Qed.
Implicit Arguments fs_injective [n x y].

Lemma bump_isn't_scum n (f : Fin n) : bump f <> scum.
  induction f.
  discriminate.
  contradict IHf.
  simpl in IHf; rewrite (fs_injective IHf).
  reflexivity.
Qed.

Lemma bump_injection n : forall u v : Fin n, bump u = bump v -> u = v.
  intros; induction n.
  apply (no_fin0 u).
  fin_case u; fin_case v.
  reflexivity.
  discriminate.
  discriminate.
  rewrite (IHn _ _ (fs_injective H)).
  reflexivity.
Qed.

Definition fin_eq_dec n (x y : Fin n) : {x = y} + {x <> y}.
intros; induction n.
apply (no_fin0 x).
fin_case x; fin_case y.
left; reflexivity.
right; discriminate.
right; discriminate.
destruct (IHn x0 x1).
left; congruence.
right; contradict n0; pose (fs_injective n0); congruence.
Defined.
Implicit Arguments fin_eq_dec [n].


(* thinning a Fin either lifts it or leaves it where it was,
 * depending on if it was above or below the wedge.
 *)
Definition thin n (wedge : Fin (S n)) : Fin n -> Fin (S n).
induction n.
refine (fun _ e => no_fin0 e _).
refine (fun wedge e =>
  match fz_or_fs wedge with
    | dyleft _ => fs e
    | dyright (exist wedge' _) =>
      match fz_or_fs e with
        | dyleft _ => fz
        | dyright (exist e' _) => fs (IHn wedge' e')
      end
  end).
Defined.

(* thickening a Fin squashes down around a pivot, this is
 * a partial inverse of thin, which will be proven soon.
 *)
Definition thicken n (wedge e : Fin (S n)) : option (Fin n).
induction n.
refine (fun _ _ => None).
refine (fun wedge e =>
  match fz_or_fs wedge with
    | dyleft _ =>
      match fz_or_fs e with
        | dyleft _ => None
        | dyright (exist e' _) => Some e'
      end
    | dyright (exist wedge' _) =>
      match fz_or_fs e with
        | dyleft _ => Some fz
        | dyright (exist e' _) =>
          match IHn wedge' e' with
            | Some e' => Some (fs e')
            | None => None
          end
      end
  end).
Defined.

Theorem thin_injective n o x y : thin n o x = thin n o y -> x = y.
  intros; induction n.
  apply (no_fin0 x).
  fin_case x; fin_case y.
  reflexivity.
  fin_case o; inversion H.
  fin_case o; inversion H.
  destruct n.
  apply (no_fin0 x0).
  fin_case o; rewrite (IHn fz x0 x1); try reflexivity; simpl.
  rewrite (fs_injective H); reflexivity.
  rewrite (IHn _ _ _ (fs_injective H)); reflexivity.
Qed.

Theorem thin_mutate n o e : thin n o e <> o.
  intros; induction n.
  apply (no_fin0 e).
  fin_case o.
  discriminate.
  fin_case e.
  discriminate.
  pose (IHn x x0).
  simpl; contradict n0.
  exact (fs_injective n0).
Qed.

Theorem thin_image n o e : o <> e -> exists e', thin n o e' = e.
  intros; induction n.
  destruct_fin o; destruct_fin e.
  absurd (@fz 1 = fz); auto.
  fin_case o.
  fin_case e.
  absurd (@fz 1 = fz); auto.
  exists x; reflexivity.
  fin_case e.
  exists fz; reflexivity.
  destruct (IHn x x0).
  contradict H; congruence.
  exists (fs x1); simpl; congruence.
Qed.

Theorem thicken_inversion n o e r : thicken n o e = r ->
  (e = o /\ r = None) + { e' | e = thin n o e' /\ r = Some e' }.
  intros; induction n.
  destruct_fin o; destruct_fin e; left; auto.
  fin_case o.
  
  fin_case e.
  left; auto.
  right; exists x; auto.
  
  fin_case e.
  right; exists fz; auto.
  
  destruct r.
  simpl in H.
  case_eq (thicken n x x0).
  intros f' eq.
  rewrite eq in *.
  injection H; clear H; intro H; rewrite <- H in *; clear H.
  destruct (IHn _ _ _ eq).
  destruct a.
  inversion H0.
  destruct s.
  destruct a.
  injection H0; clear H0; intro H0; rewrite <- H0 in *; clear H0.
  right; exists (fs f'); intuition.
  simpl; congruence.
  intro eq; rewrite eq in H; inversion H.
  
  left; intuition.
  destruct (IHn x x0 None).
  simpl in H.
  destruct (thicken n x x0); auto.
  inversion H.
  destruct a; congruence.
  destruct s.
  destruct a.
  inversion H1.
Qed.
(* Why is the proof long? *)


Definition thicken' n (wedge e : Fin (S n)) : wedge <> e -> Fin n.
intros.
pose (thicken n wedge e).
destruct (thicken_inversion n wedge e o (refl_equal _)).
destruct a; absurd (wedge = e); auto.
destruct s.
exact x.
Defined.

Lemma thick_and_thin n o e ne : e = thin n o (thicken' n o e ne).
  intros; unfold thicken'.
  set (k := thicken_inversion _ _ _ (thicken n o e) (refl_equal _)).
  destruct k.
  elimtype False; destruct a; absurd (e = o); auto.
  destruct s.
  destruct a.
  assumption.
Qed.



Require Import List.

Inductive AllDifferent A : list A -> Prop :=
| nil'  :
  AllDifferent A nil
| cons' : forall x xs,
  AllDifferent A xs -> ~In x xs -> AllDifferent A (x :: xs).
Implicit Arguments AllDifferent [A].

Lemma AllDifferent_injection A B (f : A -> B) x : (forall u v, f u = f v -> u = v) -> AllDifferent x -> AllDifferent (map f x).
  intros; induction x; simpl.
  apply nil'.
  apply cons'; inversion H0.
  apply IHx; assumption.
  contradict H4.
  destruct (in_map_iff f x (f a)).
  destruct (H5 H4).
  destruct H7.
  rewrite <- (H _ _ H7).
  assumption.
Qed.


Lemma In_P_reduce X (P : X -> Prop) o xs :
  (forall x : X, In x (o :: xs) -> P x) ->
   forall x : X, In x xs -> P x.
  intros.
  apply H.
  right.
  assumption.
Qed.

Definition map' X Y (P : X -> Prop) (f : forall x : X, P x -> Y) :
  forall xs : list X, (forall x, In x xs -> P x) -> list Y.
fix 5.
intros X Y P f xs P'.
destruct xs.
exact nil.
refine (f x (P' _ _) :: map' _ _ _ f xs (In_P_reduce _ _ _ _ P')).
left; reflexivity.
Defined.

Theorem map'_length X Y P f xs O : length xs = length (map' X Y P f xs O).
  intros; induction xs.
  reflexivity.
  simpl; rewrite (IHxs (In_P_reduce _ _ _ _ O)).
  reflexivity.
Qed.


Lemma thicken_In_inj n o a x H H' :
  In (thicken' n o a H)
     (map' _ _ (fun e => o <> e) (thicken' n o) x H') ->
  In a x.
  intros; induction x.
  inversion H0.
  simpl in H0.
  destruct H0.
  left.
  rewrite (thick_and_thin _ o a H).
  rewrite (thick_and_thin _ o a0 (H' a0 (or_introl (In a0 x) (refl_equal a0)))).
  rewrite H0.
  reflexivity.
  right.
  eapply IHx.
  apply H0.
Qed.

Lemma saturation n : forall x : list (Fin n),
  AllDifferent x -> length x = n -> forall f, In f x.
  intros; induction n.
  apply (no_fin0 f).
  destruct x.
  inversion H0.
  destruct (fin_eq_dec f f0).
  left; congruence.
  right.
  injection H0; clear H0; intro H0.
  inversion H.
  clear H1 H2 x0 xs.
  
  assert (forall e, In e x -> f0 <> e).
  intros; contradict H4; congruence.
  pose (map' _ _ _ (thicken' _ f0) x H1).
  
  Lemma AllDifferent_map'_thicken' n o x (H : (forall e, In e x -> o <> e)) :
    AllDifferent x ->
    (AllDifferent
      (map' _ _
        (fun e => o <> e)
        (thicken' n o) x
        H)).
    intros; induction x.
    apply nil'.
    simpl; apply cons'; inversion H0.
    apply IHx; assumption.
    contradict H4.
    eapply thicken_In_inj.
    apply H4.
  Qed.
  pose (AllDifferent_map'_thicken' _ _ _ H1 H3).
  
  assert (length l = n).
  rewrite <- H0.
  rewrite (map'_length _ _ _ (thicken' n f0) x H1).
  reflexivity.
  
  pose (IHn _ a H2).
  pose (i (thicken' _ f f0 n0)).
  assert (f0 <> f).
  auto.
  pose (thicken_In_inj _ f0 f x H5 H1).
  apply i1.
  apply i.
Qed.

Definition Cardinality : nat -> Set -> Prop :=
  fun n A => exists l : list A, length l = n /\ AllDifferent l.

Theorem pigeonhole_principle m : ~ Cardinality (S m) (Fin m).
  unfold Cardinality.
  intros; intro.
  destruct H; destruct H.
  destruct x.
  inversion H.
  case (In_dec (@fin_eq_dec _) f x); inversion H0.
  contradiction.
  injection H; intro H'.
  pose (saturation _ x H3 H' f).
  contradiction.
Qed.

Theorem Cardinality_n_Fin_n n : Cardinality n (Fin n).
  induction n.
  
  exists nil; split; [ reflexivity | apply nil'].
  
  destruct IHn.
  destruct H.
  exists (scum :: map (@bump _) x); split.
  
  simpl.
  rewrite map_length.
  congruence.
  
  apply cons'.
  apply AllDifferent_injection.
  apply bump_injection.
  assumption.
  clear H H0.
  induction x.
  auto.
  contradict IHx.
  inversion IHx.
  absurd (bump a = scum); auto.
  apply bump_isn't_scum.
  apply H.
Qed.

Theorem not_gt_Cardinality_n_Fin_m n m : n > m -> ~Cardinality n (Fin m).
  intros.
  
  Lemma lt_diff n m : n > m -> exists d, n = S d + m.
    unfold gt; unfold lt.
    intros n m H; induction H.
    exists 0; reflexivity.
    destruct IHle.
    exists (S x).
    rewrite H0.
    reflexivity.
  Qed.
  destruct (lt_diff n m); auto.
  rewrite H0; clear H0 H n.
  induction x.
  
  exact (pigeonhole_principle m).
  
  contradict IHx.
  destruct IHx.
  destruct H.
  inversion H0.
  rewrite <- H1 in H; inversion H.
  exists xs; split; auto.
  rewrite <- H3 in H; injection H.
  auto.
Qed.
(* Another triumph of the pigeonhole principle *)

Require Import Arith.
Theorem fin_different n m : n <> m -> Fin n <> Fin m.
  intros n m ne; intro H.
  destruct (not_eq _ _ ne);
    [ pose (Cardinality_n_Fin_n m) as p; rewrite <- H in p |
      pose (Cardinality_n_Fin_n n) as p; rewrite    H in p ];
    eapply not_gt_Cardinality_n_Fin_m;
      try apply p; auto with arith.
Qed.

Theorem fin_injective n m : Fin n = Fin m -> n = m.
  intros; destruct (eq_nat_dec n m).
  assumption.
  pose (fin_different _ _ n0); contradiction.
Qed.

cycle = concat . repeat = fix . (++)

It's annoying that I don't know how to write this totally point free.

(1)
concat . repeat
 { repeat = fix . (:) }
concat . fix . (:)
 { eta }
\x -> (concat . fix . (:)) x
 { compute }
\x -> concat (fix ((:) x))
 { f (fix g) = fix h <= f . g = h . f }
 { concat . ((:) x) = ((++) x) . concat } <- (2)
\x -> fix ((++) x)
 { eta }
fix . (++)

(2)
concat . ((:) x)
 { concat = foldr (++) [] }
foldr (++) [] . ((:) x)
 { eta }
\xs -> (foldr (++) [] . ((:) x)) xs
 { compute }
\xs -> foldr (++) [] (x:xs)
 { compute }
\xs -> x ++ (foldr (++) [] xs)
 { eta }
((++) x) . foldr (++) []
 { concat = foldr (++) [] }
((++) x) . concat

Tail calls don't exist - So why look for them?

import java.util.Stack;

interface Term { public Term whnf(); }
class Function implements Term { public Term whnf() { return this; } public Term apply(Term value) { System.out.println("Not implemented"); return null; } }

class Apply implements Term {
  Term x, y;
  boolean computed;
  Term value;
  
  public Apply(Term x, Term y) {
    this.x = x;
    this.y = y;
    computed = false;
  }
  
  /* // This is the first version of whnf I wrote, it's buggy, it crashes with a stack overflow
  public Term whnf() {
    if(!computed) {
      x = x.whnf();
      if(x instanceof Constructor) {
        value = ((Constructor)x).add(y);
      }
      else if(x instanceof Function) {
        value = ((Function)x).apply(y);
        value = value.whnf();                // this is the recursion in question, which causes it
      }
      else {
        System.out.println("ERROR");
      }
      computed = true;
    }
    return value;
  }*/
  
  public Term whnf() {
    while(true) {           // the usual fix is to use one of javas many loop constructs instead of recursion
      if(!computed) {
        x = x.whnf();
        if(x instanceof Constructor) {
          value = ((Constructor)x).add(y);
        }
        else if(x instanceof Function) {
          value = ((Function)x).apply(y);
          if(value instanceof Apply) {
            x = ((Apply)value).x;
            y = ((Apply)value).y;
            continue;
          }
        }
        else {
          System.out.println("ERROR");
        }
        computed = true;
      }
      return value;
    }
  }
}

class Constructor implements Term {
  String name;
  Term[] args;
  
  public Constructor(String name, Term... args) {
    this.name = name;
    this.args = args;
  }
  
  public Term whnf() {
    return this;
  }
  
  public Constructor add(Term t) {
    int i; Term[] oldArgs = args;
    args = new Term[oldArgs.length+1];
    for(i = 0; i < oldArgs.length; i++)
      args[i] = oldArgs[i];
    args[i] = t;
    return this;
  }
}

class Add extends Function { public Term apply(Term value) { return new Add1(value); } }
class Add1 extends Function {
  Term x;
  public Add1(Term x) { this.x = x; }
  public Term apply(Term y) {
    x = x.whnf();
    if(((Constructor)x).name == "Z") { return y; } // add Z y = y
    else if(((Constructor)x).name == "S") {        // add (S x) y = S (add x y)
      return new Constructor("S", new Apply(new Apply(new Add(), ((Constructor)x).args[0]), y));
    }
    System.out.println("Pattern match fell through");
    return null;
  }
}

class Tail extends Function { public Term apply(Term value) { return ((Constructor)value.whnf()).args[1]; } }

class ZipWith extends Function { public Term apply(Term f) { return new ZipWith1(f); } }
class ZipWith1 extends Function { Term f; public ZipWith1(Term f) { this.f = f; } public Term apply(Term xs) { return new ZipWith2(f,xs); } }
class ZipWith2 extends Function {
  Term f, xs;
  public ZipWith2(Term f, Term xs) { this.f = f; this.xs = xs; }
  public Term apply(Term ys) {
    xs = xs.whnf();
    if(((Constructor)xs).name == "[]") return ys; // zipWith f [] y = y
    ys = ys.whnf();
    if(((Constructor)ys).name == "[]") return xs; // zipWith f x [] = x
    Term x = ((Constructor)xs).args[0]; Term y = ((Constructor)ys).args[0];
    Term xss = ((Constructor)xs).args[1]; Term yss = ((Constructor)ys).args[1];
    // zipWith f (x:xss) (y:yss) = f x y : zipWith f xss yss
    return new Constructor(":", new Apply(new Apply(f,x), y), new Apply(new Apply(new Apply(new ZipWith(), f), xss), yss));
  }
}

class F extends Function { public Term apply(Term x) { return new Apply(new F(), x); } }

interface Instruction { public void execute(Stack<Instruction> todo); }

class OpenBracket implements Instruction {
  public void execute(Stack<Instruction> todo) {
    System.out.print("(");
  }
}

class CloseBracket implements Instruction  {
  public void execute(Stack<Instruction> todo) {
    System.out.print(")");
  }
}

class EvalTerm implements Instruction {
  Term t;
  
  public EvalTerm(Term t) {
    this.t = t;
  }
  
  public void execute(Stack<Instruction> todo) {
    Constructor c = (Constructor)t.whnf();
    t = c;
    
    System.out.print(c.name + " ");
    
    todo.push(new CloseBracket());
    for(int i = c.args.length-1; i >= 0; i--) {
      todo.push(new EvalTerm(c.args[i]));
    }
    todo.push(new OpenBracket());
  }
}

class Evaluator {
  Stack<Instruction> todo;
  
  public Evaluator(Term program) {
    todo = new Stack<Instruction>();
    todo.push(new EvalTerm(program));
  }
  
  public void evaluate() {
    while(!todo.empty()) todo.pop().execute(todo);
  }
}

public class NoTCO {
  public static void main(String args[]) {
    Term one = new Apply(new Constructor("S"), new Constructor("Z"));
    Term two = new Apply(new Constructor("S"), new Apply(new Constructor("S"), new Constructor("Z")));
    Term four = new Apply(new Constructor("S"), new Apply(new Constructor("S"), new Apply(new Constructor("S"), new Apply(new Constructor("S"), new Constructor("Z")))));
    
    // 1 : 1 : zipWith (+) fibs (tail fibs)
    Term fibs =
      new Apply(new Apply(new Constructor(":"), one),
        new Apply(new Apply(new Constructor(":"), one),
          null));
    ((Apply)((Apply)fibs).y).y =
      new Apply(new Apply(new Apply(new ZipWith(), new Add()), fibs), new Apply(new Tail(), fibs));
    
    //new Evaluator(fibs).evaluate();
    new Evaluator(new Apply(new F(), new Constructor("3"))).evaluate();
    System.out.println();
  }
}


// Important thing to note is,
// 1) This code does not analyze the input program to detect and 'optimize' tail recursion
// 2) This program doesn't stack overflow when evaluating a "tail recursive" program
//
// NB. I put "tail recursive" in quotes because it's actually irrelevant that the code is what you'd call in a strict language by that term
//     as I said in my previous post, the reason it doesn't stack overflow is not at all related to that.

Tail Call Optimization doesn't exist in Haskell

It's well known that since Haskell programs are evaluated lazily, the
considerations for writing recursive code are different to those of a strict
language.

> cat (zero,plus) [] = zero
> cat (zero,plus) (x:xs) = x `plus` cat (zero,plus) xs

> cat' (zero,plus) [] acc = acc
> cat' (zero,plus) (x:xs) acc = cat' (zero,plus) xs (acc `plus` x)

> loads = [1..1000000]

*Main> cat (0,(+)) loads
*** Exception: stack overflow
*Main> cat' (0,(+)) loads 0
*** Exception: stack overflow


Since normal numbers in haskell are strict, I'm going to use lazy numbers here
(The hope is that any results should apply to lazy structures in general, and
avoid having to take strictness into account).

> data N = Z | S N     deriving Show

> zero = Z
> plus (S x) y = S (plus x y)
> plus   Z   y = y

> lots = take 1000000 . iterate S $ Z

*Main> cat (zero,plus) lots
S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S^C(S (S (S (S Interrupted.
*Main> cat' (zero,plus) lots Z
*** Exception: stack overflow


Another example is an infinite loop:

*Main> let f x = f x in f []
^CInterrupted.
*Main> let f x = f (():x) in f []
^CInterrupted.

Both continue happily, the second takes up huge amounts of memory but it does
not stack overflow.

Haskell evaluation is like graph reduction, a program is a graph which you tug
on the end until you get a weak head normal form, in these cases you never get
one, but the program/graph is stored on the heap, in the second case that data
gets bigger and bigger (it might even get swapped to the hard disk after a
while).

That's why they didn't crash, and it had nothing to do with tail calls or tail
call optimization,  cat (zero,plus) lots  didn't do any tail call and that
didn't crash. The reason any stack overflow occurs is that the program which
reduces the graph (on the heap) has a stack, that program in my case GHC is
written in C (the RTS) and when it delves deep into an expression such as
1 + (2 + (3 + (4 + ...)))   that is what builds up stack.



So why does something like:

> spam = putStr "SPAM " >> spam

never crash?

Since (>>) is in tail position (spam is not a tail call), again, tail calls have
nothing to do with this.  m >> n  in this case means do m throw away the result
then do n, it must get thrown to the garbage collector (unlike the  f (():x)
example where the value can't be collected).



That's all fine, but we still haven't been able to sum  [1..1000000]  together.
So to recap, building up a huge expression on the heap is fine (as in the
cat (zero,plus) lots  example) but walking deep into an expression without
getting any constructors is dangerous.

> kat' (zero,plus) [] acc = acc
> kat' (zero,plus) (x:xs) acc = acc'plus'x `seq` kat' (zero,plus) xs acc'plus'x
>  where acc'plus'x = acc `plus` x

*Main> cat' (0,(+)) loads 0
*** Exception: stack overflow
*Main> kat' (0,(+)) loads 0
500000500000


> -- And a huge thanks to everyone that I talked about this with
> -- for bending my mind :)

Unscrambling without Prolog

Inductive Bit : Set :=
  H  | V
| TL | TR
| BL | BR.

Definition State :=
 (Bit * Bit * Bit *
  Bit *       Bit *
  Bit * Bit * Bit)%type.

Inductive Move : State -> State -> Set :=
| refl : forall S, Move S S

| top_left : forall A B C D E F G H, Move
  (A, B, C,
   D,    E,
   F, G, H)
  (B, C, A,
   D,    E,
   F, G, H)

| left_down : forall A B C D E F G H, Move
  (A, B, C,
   D,    E,
   F, G, H)
  (F, B, C,
   A,    E,
   D, G, H)

| right_down : forall A B C D E F G H, Move
  (A, B, C,
   D,    E,
   F, G, H)
  (A, B, H,
   D,    C,
   F, G, E)

| bottom_left : forall A B C D E F G H, Move
  (A, B, C,
   D,    E,
   F, G, H)
  (A, B, C,
   D,    E,
   G, H, F)

| trans_closure : forall A M Z,
  Move A M -> Move M Z -> Move A Z.


Definition solution state := Move state (TL, H, TR,
                                         V,     V,
                                         BL, H, BR).

Theorem prolog_example :
  solution (H, BR, BL,
            H,     TL,
            TR, V, V).


unfold solution.
eapply trans_closure.
apply top_left.
change (solution (BR, BL, H, H, TL, TR, V, V)).

Ltac whack direction :=
  unfold solution;
  eapply trans_closure;
    [ apply direction
    | match goal with
        | |- Move ?x _ => change (solution x)
      end
    ].

Ltac wtop := whack top_left.
Ltac wleft := whack left_down.
Ltac wright := whack right_down.
Ltac wbottom := whack bottom_left.

wtop.
wtop.

wtop.
wtop.
wbottom.
wbottom.
wleft.
wright.
wbottom.
wbottom.
wleft.
wright.

unfold solution.

apply refl.

Qed.

Theorem automated_example :
  solution (H, BR, BL,
            H,     TL,
            TR, V, V).

Inductive Marker (A : State) : Set := mkMarker.

Ltac save_state :=
  match goal with
    | |- solution ?state =>
      let seen := fresh "seen"
        in pose (seen := mkMarker state)
  end.

Ltac check_progress :=
  match goal with
    | |- solution ?State =>
      match goal with
        | _ : Marker State |- _ =>
          pose (dead_end := True)
        | _ => idtac
      end
  end.

Ltac swtop := save_state; whack top_left; check_progress.
Ltac swleft := save_state; whack left_down; check_progress.
Ltac swright := save_state; whack right_down; check_progress.
Ltac swbottom := save_state; whack bottom_left; check_progress.

Ltac swhack n :=
  (unfold solution; apply refl) ||
    match n with
      | 0 => fail
      | S ?m => swtop; pose (dead_end := False); clear dead_end; swhack m
      | S ?m => swleft; pose (dead_end := False); clear dead_end; swhack m
      | S ?m => swright; pose (dead_end := False); clear dead_end; swhack m
      | S ?m => swbottom; pose (dead_end := False); clear dead_end; swhack m
    end.

swhack 12.

Defined.

Print automated_example.

(*
automated_example = 
let seen := mkMarker (H, BR, BL, H, TL, TR, V, V) in
trans_closure (H, BR, BL, H, TL, TR, V, V) (BR, BL, H, H, TL, TR, V, V)
  (TL, H, TR, V, V, BL, H, BR) (top_left H BR BL H TL TR V V)
  (let dead_end := False in
   let seen0 := mkMarker (BR, BL, H, H, TL, TR, V, V) in
   trans_closure (BR, BL, H, H, TL, TR, V, V) (BL, H, BR, H, TL, TR, V, V)
     (TL, H, TR, V, V, BL, H, BR) (top_left BR BL H H TL TR V V)
     (let dead_end0 := False in
      let seen1 := mkMarker (BL, H, BR, H, TL, TR, V, V) in
      trans_closure (BL, H, BR, H, TL, TR, V, V) (TR, H, BR, BL, TL, H, V, V)
        (TL, H, TR, V, V, BL, H, BR) (left_down BL H BR H TL TR V V)
        (let dead_end1 := False in
         let seen2 := mkMarker (TR, H, BR, BL, TL, H, V, V) in
         ...
*)

Require Import List.
Inductive Move2 : Set := top_left2 | left_down2 | right_down2 | bottom_left2.
Fixpoint display_moves p q (m : Move p q) : list Move2 :=
  match m with
    | refl _ => nil
    | top_left _ _ _ _ _ _ _ _ => top_left2::nil
    | left_down _ _ _ _ _ _ _ _ => left_down2::nil
    | right_down _ _ _ _ _ _ _ _ => right_down2::nil
    | bottom_left _ _ _ _ _ _ _ _ => bottom_left2::nil
    | trans_closure _ _ _ x y => display_moves _ _ x ++ display_moves _ _ y
  end.

Eval compute in (display_moves _ _ automated_example).
(*
     = top_left2
       :: top_left2
       :: left_down2
       :: top_left2
       :: right_down2
       :: top_left2
       :: top_left2
       :: bottom_left2
       :: bottom_left2
       :: left_down2
       :: right_down2
       :: right_down2
       :: nil
     : list Move2
*)

Unscrambling with Prolog

%% I'm playing this Oxyd game (inside Enigma [link])
%% One of the puzzles is this scrambled configuration

starting(([-,⌋,⌊]
         ,[-,  ⌈]
         ,[⌉,|,|])).

%% And you've to hit against the sides to unscramble it into:

solution(([⌈,-,⌉]
         ,[|,  |]
         ,[⌊,-,⌋])).

%% Then it explodes and you win a spring
%% The moves you can do are:

move(top_left,
    ([A,B,C]
    ,[D,  E]
    ,[F,G,H]) --> ([B,C,A]
                  ,[D,  E]
                  ,[F,G,H])).

move(left_down,
    ([A,B,C]
    ,[D,  E]
    ,[F,G,H]) --> ([F,B,C]
                  ,[A,  E]
                  ,[D,G,H])).

move(right_down,
    ([A,B,C]
    ,[D,  E]
    ,[F,G,H]) --> ([A,B,H]
                  ,[D,  C]
                  ,[F,G,E])).

move(bottom_left,
    ([A,B,C]
    ,[D,  E]
    ,[F,G,H]) --> ([A,B,C]
                  ,[D,  E]
                  ,[G,H,F])).

%% I want Prolog to solve this automatically for me though,
%% My first attempt is to use recursion like so,

%: solve(Win,[]) :- solution(Win).
%: solve(State,[Move|Moves]) :- move(Move,State --> Next), solve(Next,Moves).

%! ?- starting(State), solve(State,Moves).
%! ERROR: Out of local stack

%% Since Prolog searches depth first, this just kept trying top_left,
%% again and again, getting nowhere, infact it seeing the same config.
%% so I can pass along a list of seen configurations now, and fail when
%% the same one is seen twice.

%: solve(Win,[],_) :- solution(Win).
%: solve(State,[Move|Moves],Seen) :- move(Move,State --> Next), not(member(Next,Seen)), solve(Next,Moves,[State|Seen]).

%! ?- starting(State), solve(State,Moves,[State]).
%! State = ([-, '⌋', '⌊'], [-, '⌈'], ['⌉', ('|'), ('|')]),
%! Moves = [top_left, top_left, left_down, top_left, top_left, left_down, ...]

%% I got a solution this time... but it's thousands of moves, I think the puzzle can be solved
%% Within at least 10 moves, so Prolog should fail if it gets into a branch in the search tree that deep

solve(Win,[],_,_) :- solution(Win).
solve(State,[Move|Moves],Seen,Limit) :-
 move(Move,State --> Next), not(member(Next,Seen)), succ(LowerLimit,Limit), solve(Next,Moves,[State|Seen],LowerLimit).

solve(Solution) :- starting(State), solve(State,Solution,[State],10).

%! ?- solve(Moves).
%! Moves = [top_left, top_left, bottom_left, bottom_left, left_down, right_down, bottom_left,
%!          bottom_left, left_down, right_down].

Lights out solver using CLP

:- use_module(library(clpfd)).

solve(Puzzle,Solution) :-
 dimensions(Puzzle,Rows,Cols), dimensions(Solution,Rows,Cols),
 flatten(Solution,Variables), Variables ins 0..1,
 cells_of(Puzzle --> configure(Solution)), label(Variables).

configure(Solution,(X,Y,o)) :- around(X,Y,Solution,Group), off(Group).
configure(Solution,(X,Y,*)) :- around(X,Y,Solution,Group), on(Group).

on(Lights) :- sum(Lights, #=, On), 1 #= On mod 2.
off(Lights) :- sum(Lights, #=, Off), 0 #= Off mod 2.

around(X,Y,Grid,[Up,Left,Down,Right,Middle]) :-
 Yu is Y-1, Xl is X-1,
 Yd is Y+1, Xr is X+1,
 ( Grid@([Yu,X]->Up) -> true ; Up = 0 ),
 ( Grid@([Y,Xl]->Left) -> true ; Left = 0 ),
 ( Grid@([Yd,X]->Down) -> true ; Down = 0 ),
 ( Grid@([Y,Xr]->Right) -> true ; Right = 0 ),
 ( Grid@([Y,X]->Middle) -> true ; Middle = 0 ).

game([[*,o,o,o,o,o,*,o],
      [*,*,o,*,*,*,*,*],
      [*,*,o,*,*,*,o,*],
      [*,o,o,o,o,o,o,o],
      [o,*,*,o,o,o,*,*],
      [o,*,o,o,o,o,o,o],
      [*,*,*,*,*,*,o,o],
      [o,*,*,*,*,*,*,*]]).





:- op(500,xfy,@).
:- op(1050,yfx,<-).

flatten([],[]).
flatten([X|Xs],Zs) :- flatten(Xs,Ys), append(X,Ys,Zs).

flip(P,Y,X) :- call(P,X,Y).
dimensions(Grid, Rows, Cols) :- length(Grid, Rows), maplist(flip(length,Cols),Grid).

E@([]->E)         :- !.
[X|_]@([0|Ns]->E) :- !, X@(Ns->E).
[_|X]@([N|Ns]->E) :- !, N > 0, succ(M, N), X@([M|Ns]->E).

_/E@([]<-E)               :- !.
[X|Xs]/[Y|Xs]@([0|Ns]<-E) :- !, X/Y@(Ns<-E).
[X|Xs]/[X|Ys]@([N|Ns]<-E) :- !, N > 0, succ(M, N), Xs/Ys@([M|Ns]<-E).

tuple(Board,Tuples) :- tuple((0,0),Board,Tuples).
tuple(_,[],[]).
tuple((X,Y),[Row|Rows],Tuples) :-
 tuprow((X,Y),Row-Tail,Tuples),
 succ(Y,Y1), tuple((X,Y1),Rows,Tail).
tuprow(_,[]-X,X).
tuprow((I,J),[E|Es]-X,[(I,J,E)|Xs]) :- succ(I,I1),tuprow((I1,J),Es-X,Xs).

cells_of(Grid --> Pred) :- tuple(Grid, Tuples), maplist(Pred, Tuples).