Short Note on Semantics

With all curious derivations that come from the forests of To Mock a Mockingbird, and in the intrests of deepening understanding of type theory (in particular CIC) we considered axiomatizing the SK calculus in Coq.

Module Type SK.
  (* axiomatization of the theory *)
  Parameter SK : Set.

  Parameter app : SK -> SK -> SK.
  Infix "*" := app.
  
  Parameter S : SK.
  Parameter K : SK.
  
  Axiom S_prop : forall a b c, S * a * b * c = (a * c) * (b * c).
  Axiom K_prop : forall a b, K * a * b = a.
End SK.

It is not defined as an inductive type (as you might usually do) because there is no normal form for SK that we can compute terms into inside Coq (we would have to equate diverging terms with an "omega" symbol for a start, which is well known to be a partial operation). It would be possible to use a non-normal forma and quotient it out with a special (undecidable) equivalence relation, but we do not this.. Instead the axioms of the theory are given, One immediately notices that there is a trivial model of these axioms:

Module SK_trivial_model : SK.
  (* one model (giving non-contradiction of the theory) *)
  Definition SK := unit.
  
  Definition app := fun (_ _ : unit) => tt.
  Infix "*" := app.
  
  Definition S := tt.
  Definition K := tt.
  
  Theorem S_prop : forall a b c, S * a * b * c = (a * c) * (b * c).
    reflexivity.
  Qed.
  
  Theorem K_prop : forall a b, K * a * b = a.
    destruct a; reflexivity.
  Qed.
End SK_trivial_model.

(This implementation mostly serves to show the syntax and so on of how to construct a model of a theory inside Coq).

Anyway, we eliminate trivial models by saying that S <> K.

  Axiom SK_prop : S <> K.

We could now develop the theory of combinator calculus, prove things like S <> I and so forth.

Module SK_theory <: SK.
  Include Type SK.
  
  (* Development of the theory of SK calculus, valid for all models *)
  
  Ltac sk := repeat (rewrite S_prop || rewrite K_prop).
  
  Definition I := S * K * S.
  Theorem I_prop : forall x, I * x = x.
    intros; unfold I; sk; reflexivity.
  Qed.
  Ltac ski := repeat (sk || rewrite I_prop).
  
  Theorem IK : I <> K.
    Definition F x y b := b * K * I * x * y.
    
    intro Eq; generalize (f_equal (F K S) Eq); unfold F; ski.
    apply SK_prop.
  Qed.
  
  Definition U := S * I * I.
  Theorem U_prop : forall x, U * x = x * x.
    intros; unfold U; ski; reflexivity.
  Qed.
  
  Ltac skiu := repeat (ski; rewrite U_prop).
End SK_theory.

As fun as that would be, I don't believe you could ever reach a contradiction by assuming the SK theory. Yet no model exists inside Coq!

This is a rather confusing and troubling state, but Russell O'Connor mentioned to me the possibility of giving an interpretation of CIC into a theory that has a Halting-Oracle and that solves it! This is surely a valid interpretation of CIC, it's just got this SK theory added in with the usual stuff - the halting oracle would be used to normalize SK terms and prove satisfy our theory. So despite the non-existence of a model of SK inside Coq: It appears we can reason about the SK calculus directly. (Rather than a halting oracle you might have considered a special equivalence relation being interpreted for the congruence of SK objects but lets pretend Coq has Axiom K so that need not be considered).

This is all very interesting to me because it seems to suggest mathematics existing outside of the formal theory we work in or study. Something I never believed in - It's not completely clear if this is profound or if I am just going soft.

Strongly Specified Parser Combinators

Following the approach Wouter Swierstra used for Hoare State Monad, we define a Parser monad with pre and post conditions that express soundness (but not completeness) of the parser.

The computational aspect of it is the same old parser monad, type Parser s a = [s] -> [(s, [a])], which takes a list of tokens [s] to a (possibly empty) list (here is where backtracking/nondeterminism comes into it) of parses paired with the rest of the text. It's a monad and also a monad plus.

On the specification end, we can put a precondition on the input string (for example, you might say the input length is <= some value, for ensuring termination of a recursive parser) and also a post condition comparing the input with the parsed value and the remaining output.

  Definition Pre := list s -> Prop.
  Definition Post (t : Set) := list s -> t -> list s -> Prop.
  
  Program Definition Parser (pre : Pre) (t : Set) (post : Post t) : Set :=
      forall i : { t : list s | pre t }, list ({ (x, r) : t * list s | post i x r }).

in Haskell we might define:

m >>= f = \i -> concatMap (uncurry f) (m i)

And in Coq, using Program we have roughly the same thing. Except that one has to apply a 'noncomputational_map' to fudge the proofs paired up with the list elements.

  Program Definition Bind (a b : Set) P1 P2 Q1 Q2
    (m : Parser P1 a Q1)
    (f : (forall x : a, Parser (P2 x) b (Q2 x))) :
    Parser (fun i => P1 i /\ forall x o, Q1 i x o -> P2 x o)
           b
           (fun i x' o' => exists x o, Q1 i x o /\ Q2 x o x' o') :=
    fun i => @flat_map ({ (x, o) : a * list s | Q1 i x o }) _
      (fun xo => match xo with (x,o) => noncomputational_map _ _ _ _ (f x o) end)
      (m i).

Seeing as noncomputational map doesn't do anything, we prove a theorem expressing that as justification for extracting it out as the identity function (rather it being equivalent to map id traversing the whole list).

  Theorem noncomputational_map_identity :
    forall l,
      map (@proj1_sig _ _) l = map (@proj1_sig _ _) (noncomputational_map l).
  
  Extract Inlined Constant noncomputational_map => "id".

Another nice parser combinator is the fixed point of a parser:

  Program Definition Fix t {P Q} :
    (forall i : { t : list s | P t },
      Parser (fun i' => length i' < length i /\ P i') t Q ->
      list ({ (x, o) : t * list s | Q i x o })) ->
    Parser P t Q :=
    fun Rec =>
      well_founded_induction
        (well_founded_ltof ({ i : list s | P i }) (fun i => length i))
        (fun i => list ({ (x, o) : t * list s | Q i x o }))
        (fun x Rec' => Rec x (fun i => Rec' i _)).

It packages up well founded recursion on the size of the input string, so that any non-left recursive parsers should be easily defined.

Enough of the heavy machinary! A simple example of putting thing into work now:

 <par> ::= <epsilon> | '(' <par> ')' <par>

To parse this we define a type of tokens and abstract syntax of parsing derivations - then relate them with a function:

  Inductive token := open | close.
  Inductive par := epsilon : par | wrappend : par -> par -> par.

  Fixpoint print (p : par) : list token :=
    match p with
      | epsilon => nil
      | wrappend m n => (open::nil) ++ print m ++ (close::nil) ++ print n
    end.

Now Program lets us define the par parser as the fixed point of the sum of epsilon and wrapped recursions:

  Program Definition par_parser : Parser token (fun _ => True) par (fun x p y => x = print p ++ y /\ length y <= length x) :=
    Fix token par (fun i parRec =>
      Plus _ _ (fun i' => i = i') _
        (fudge_pre_and_post_conditions _ _ _
          (Return epsilon))
        (fudge_pre_and_post_conditions _ _ _
          (Symbol token eq_token_dec open >>= fun _ =>
           parRec >>= fun m =>
           Symbol token eq_token_dec close >>= fun _ =>
           parRec >>= fun n =>
           Return (wrappend m n)))
      i).

Here are the actual scripts http://github.com/odge/parseq/tree/master

How to halve a number

(*
 * How to halve a number
 * ---------------------
 *)

(* (* just so we start on the same page, what is a number? *)
 *
 * Inductive nat : Set :=
 * | O : nat
 * | S : nat -> nat.
 *)

Module Type Halver.
  
  Parameter half : nat -> nat.
  
  Axiom e1 : half 0 = 0.
  Axiom e2 : half 1 = 0.
  Axiom e3 : forall n, half (S (S n)) = S (half n).

  (* An equational specification is given as a module
   * so now it is possible it give various implementations
   *)

End Halver.

Module By_Default : Halver.
  
  Fixpoint half (n : nat) : nat :=
    match n with
      | O => O
      | S O => O
      | S (S n) => S (half n)
    end.
  
  Definition e1 : half 0 = 0 := refl_equal _.
  Definition e2 : half 1 = 0 := refl_equal _.
  Definition e3 n : half (S (S n)) = S (half n) := refl_equal _.

  (* This is the sort of thing one would normally start with,
   * pattern match on a term and use recursive calls on a
   * structurally smaller term, the idea of 'structurally smaller'
   * is part of the type rules actually and it is the transitive
   * closure of   (1) p_i < C p_1 p_2 ... p_n
   *        and   (2) f x < f
   * rule (1) and (2) say that a term in smaller than any
   * construction built from it, a construction being something
   * literally built from constructor or a function
   *)

End By_Default.

Module By_Divine_Inspiration : Halver.
  
  (* Definition half n :=
   *    fst (nat_rect (fun _ => (nat * nat)%type)
   *      (O, O)
   *      (fun n Pn => let (p,q) := Pn in (q, S p))
   *      n).
   * (* it seems impossible to prove this one correct *)
   *)
  
  Definition half n :=
    fst (nat_rect (fun _ => (nat * nat)%type)
      (O, O)
      (fun n Pn => (snd Pn, S (fst Pn)))
      n).
  
  Definition e1 : half 0 = 0 := refl_equal _.
  Definition e2 : half 1 = 0 := refl_equal _.
  Definition e3 n : half (S (S n)) = S (half n) := refl_equal _.

End By_Divine_Inspiration.

Module By_Devising_Data : Halver.
  
  (* This way seems like a 'view' in the sense of Wadler,
   * The structure of the data make the program definition
   * straight-forward.
   *)
  
  Inductive nat' : Set :=
  | Zero : nat'
  | One : nat'
  | SuccSucc : nat' -> nat'.
  
  Definition zero := Zero.
  Fixpoint succ (n : nat') :=
    match n with
      | Zero => One
      | One => SuccSucc Zero
      | SuccSucc n => SuccSucc (succ n)
    end.
  
  Fixpoint nat_to_nat' (n : nat) : nat' :=
    match n with
      | O => zero
      | S n => succ (nat_to_nat' n)
    end.
  
  Fixpoint half' (n : nat') : nat :=
    match n with
      | Zero => O
      | One => O
      | SuccSucc n => S (half' n)
    end.
  
  Definition half n := half' (nat_to_nat' n).
  
  Definition e1 : half 0 = 0 := refl_equal _.
  Definition e2 : half 1 = 0 := refl_equal _.
  
  Lemma succ_succs n : succ (succ n) = SuccSucc n.
    induction n; simpl; try reflexivity.
    rewrite IHn; reflexivity.
  Qed.
  
  Theorem e3 n : half (S (S n)) = S (half n).
    intro n.
    unfold half.
    simpl.
    rewrite succ_succs.
    reflexivity.
  Qed.

End By_Devising_Data.

Module By_Mutual_Induction : Halver.
  
  Inductive Even : nat -> Set :=
  | EvenO : Even O
  | EvenS n : Odd n -> Even (S n)
  with      Odd : nat -> Set :=
  | OddS n : Even n -> Odd (S n).
  
  Fixpoint even_or_odd n : Even n + Odd n :=
    match n as n return Even n + Odd n with
      | O => inl _ EvenO
      | S n =>
        match even_or_odd n with
          | inl even => inr _ (OddS _ even)
          | inr odd => inl _ (EvenS _ odd)
        end
    end.
  
  Fixpoint halfE n (e : Even n) : nat :=
    match e with
      | EvenO => O
      | EvenS n odd => S (halfO n odd)
    end
  with     halfO n (o : Odd n) : nat :=
    match o with
      | OddS n even => halfE n even
    end.
  
  Definition half (n : nat) : nat :=
    match even_or_odd n with
      | inl even => halfE n even
      | inr odd => halfO n odd
    end.
  
  (* Proving this program correct is quite a lot
   * of work compared to the previous implementations,
   * these tricky inversion lemmas which would be trivial
   * to prove using pattern matching at least show some
   * techniques.
   *)
  
  Lemma unique_lemma_1 (e : Even 0) : e = EvenO.
    intro e.
    refine (
      match e as e' in Even Zero return
        match Zero return Even Zero -> Prop with
          | O => fun e'' : Even 0 => e'' = EvenO
          | S _ => fun _ => True
        end e'
        with
        | EvenO => refl_equal _
        | EvenS _ _ => I
      end
    ).
  Qed.
  
  Lemma unique_lemma_2 n (e : Even (S n)) : { o' : _ | e = EvenS n o' }.
    intros n e.
    refine (
      match e as e' in Even SuccN return
        match SuccN return Even SuccN -> Set with
          | O => fun _ => True
          | S n => fun e' : Even (S n) =>
            { o' : _ | e' = EvenS n o' }
        end e'
        with
        | EvenO => I
        | EvenS n' o' => exist _ o' (refl_equal _)
      end
    ).
  Qed.
  
  Lemma unique_lemma_3 n (o : Odd (S n)) : { e' : _ | o = OddS n e' }.
    intros n o.
    refine (
      match o as o' in Odd SuccN return
        match SuccN return Odd SuccN -> Set with
          | O => fun _ => True
          | S n => fun o' : Odd (S n) =>
            { e' : _ | o' = OddS n e' }
        end o'
        with
        | OddS n' e' => exist _ e' (refl_equal _)
      end
    ).
  Qed.
  
  (* There is only one way to prove a number is Even
   * and similarly to prove it's Odd
   *)
  
  Theorem unique_classificationE n (e e' : Even n) : e = e'
  with    unique_classificationO n (o o' : Odd n) : o = o'.
    induction n; intros.
    
    rewrite unique_lemma_1 with e.
    rewrite unique_lemma_1 with e'.
    reflexivity.
    
    destruct (unique_lemma_2 _ e) as [o eq].
    destruct (unique_lemma_2 _ e') as [o' eq'].
    rewrite eq; rewrite eq'.
    rewrite (unique_classificationO n o o').
    reflexivity.
    
    destruct n.
    intro H; inversion H.
    intros.
    destruct (unique_lemma_3 _ o) as [e eq].
    destruct (unique_lemma_3 _ o') as [e' eq'].
    rewrite eq; rewrite eq'.
    rewrite (unique_classificationE n e e').
    reflexivity.
  Qed.
  
  Lemma halfE_SS n e e' : halfE (S (S n)) e' = S (halfE n e)
  with  halfO_SS n o o' : halfO (S (S n)) o' = S (halfO n o).
  intros.
  destruct (unique_lemma_2 _ e') as [o eq].
  destruct (unique_lemma_3 _ o) as [e'' eq'].
  subst.
  simpl.
  assert (e = e'') as E by apply unique_classificationE.
  rewrite E; reflexivity.
  
  intros.
  destruct (unique_lemma_3 _ o') as [e eq].
  destruct (unique_lemma_2 _ e) as [o'' eq'].
  subst.
  simpl.
  assert (o = o'') as O by apply unique_classificationO.
  rewrite O; reflexivity.
  Qed.
  
  Definition which P Q : P + Q -> bool :=
    fun choice =>
      match choice with
        | inl _ => true
        | inr _ => false
      end.
  Lemma even_or_odd_SS n : which _ _ (even_or_odd (S (S n))) = which _ _ (even_or_odd n).
    induction n.
    reflexivity.
    simpl in *.
    destruct (even_or_odd n).
    reflexivity.
    reflexivity.
  Qed.
  
  Definition e1 : half 0 = 0 := refl_equal _.
  Definition e2 : half 1 = 0 := refl_equal _.
  Theorem e3 n : half (S (S n)) = S (half n).
    intro n.
    unfold half.
    generalize (even_or_odd_SS n).
    destruct (even_or_odd n); destruct (even_or_odd (S (S n)));
      simpl; intro hyp; try discriminate hyp.
    apply halfE_SS.
    apply halfO_SS.
  Qed.

End By_Mutual_Induction.

Module By_Well_Founded_Induction : Halver.
  
  Section Well_Founded_Relations.
    
    Variable A : Type.
    Variable R : A -> A -> Prop.
    
    Inductive Acc (x : A) : Prop :=
    | below : (forall y : A, R y x -> Acc y) -> Acc x.
    
    (* x must be a parameter (instead of Acc : A -> Prop) for
     * Set/Type elimination, but why?
     *)
    
    Definition Well_Founded := forall x : A, Acc x.
    
    Inductive Transitive_Closure : A -> A -> Prop :=
    | step x y : R x y -> Transitive_Closure x y
    | transitivity x y z : R x y -> Transitive_Closure y z -> Transitive_Closure x z.
    
    Definition Well_Founded_Induction
      (W : Well_Founded)
      (P : A -> Type)
      (rec : forall x, (forall y, R y x -> P y) -> P x)
      : forall a, P a :=
        fun a => Acc_rect P (fun x _ hyp => rec x hyp) a (W a).
  
  End Well_Founded_Relations.
  
  Section Transitive_Relation.
    
    Variable A : Type.
    Variable R : A -> A -> Prop.
    
    Theorem Transitive_Closure_Well_Founded :
      Well_Founded A R -> Well_Founded A (Transitive_Closure A R).
    Proof.
      unfold Well_Founded; intros R_Acc x.
      
      induction (R_Acc x) as [x R_ind T_ind].
      
      apply below; intros y Trans.
      
      induction Trans.
      
      apply T_ind; assumption.
      
      pose (IHTrans R_ind T_ind) as IH; inversion IH as [H']; subst.
      apply H'.
      apply step.
      assumption.
    Defined.
  
  End Transitive_Relation.
  
  Section Nat_Structural_Measure.
    
    (* Looking at the definition of nat: *)
    
    (*
     * Inductive nat : Set :=
     * | O : nat
     * | S : nat -> nat.
     *)
    
    (* shows there is one (simple) recursive field *)
    
    Inductive nat_step : nat -> nat -> Prop :=
    | nat_step_a : forall x, nat_step x (S x).
    
    (* the nat_step relation expresses this recursion
     * every inductive type admits a step relation
     * (indexed inductives define indexed relations,
     * but maybe wrappig them in sigT would be better?)
     *)
    
    Theorem nat_step_Well_Founded : Well_Founded nat nat_step.
      
      unfold Well_Founded.
      
      induction x;
        apply below; intros y Ry.
      
      inversion Ry.
      
      inversion Ry.
      subst.
      assumption.
    
    Defined.
    
    (* Could one generically define all Φ_step relations,
     * and give a generic proof that they are all Well_Founded?
     *)
    
    (* The transitive closure of the step relation corresponds to
     * the usual idea of lt/(<) on nat:
     *)
    
    Definition nat_struct := Transitive_Closure nat nat_step.
    Definition nat_struct_Well_Founded :=
      Transitive_Closure_Well_Founded nat nat_step nat_step_Well_Founded.
    
    (* In general terms it is a typed version of the 'structurally smaller'
     * relation in the metatheory which lets definitions like the one in
     * By_Default be accepted
     *)
  
  End Nat_Structural_Measure.
  
  (* Now the equations we want to satisy are: *)
  
  (*
   * half O := O
   * half (S O) := O
   * half (S (S n)) := S (half n)
   *)
  
  (* so in terms of (toned down) eliminators that is:
   * 
   * half n := nat_case n
   *            O
   *            (fun n' Pn' =>
   *              nat_case n'
   *               O
   *               (fun n'' Pn'' =>
   *                 S (half n''))).
   * 
   * clearly that definition is not acceptable with
   *  no termination argument what-so-ever! so to
   *  rectify that, we can let P express that this
   *  number is smaller than n, and use well founded
   *  induction on the size measure.
   *)
  
  Lemma SSsmaller m : nat_struct m (S (S m)).
    intro m.
    apply transitivity with (S m).
    constructor.
    apply step.
    constructor.
  Defined.
  
  Definition half := Well_Founded_Induction nat nat_struct nat_struct_Well_Founded
    (fun _ => nat)
    (nat_rec (fun x => (forall y : nat, nat_struct y x -> nat) -> nat)
      (fun rec => O)
      (fun n Pn rec =>
        nat_rec (fun x => (forall y : nat, nat_struct y (S x) -> nat) -> nat)
        (fun rec => O)
        (fun m Pm rec => S (rec m (SSsmaller m)))
        n
        rec)).
  
  (*
   * The definition may look a bit complicated but I think this could
   *  be computed automatically from the equational specification,
   *  the method seems like a good way to compile dependent pattern matching
   *  into a basic type theory though, so that we don't have to use something
   *  like a 'match' construct.
   *)
  
  Definition e1 : half 0 = 0 := refl_equal _.
  Definition e2 : half 1 = 0 := refl_equal _.
  Definition e3 n : half (S (S n)) = S (half n) := refl_equal _.
  
  (*
   * It's not luck (at least I think it's not, and I really hope so)
   *  that the recursive equality is provable by reflexivity, but it
   *  does require the SSsmaller proof term to be canonical (made up
   *  of constructors), since every proof that a term is structurally 
   *  smaller than another can be a canonical proof that poses no
   *  problem. I don't yet know how it will interact with dependent
   *  pattern match specialization though. (I can't think of any
   *  functions over inductive families that aren't 'step' recursive
   *  though, does anyone know of some examples?)
   *)

End By_Well_Founded_Induction.

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

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

Semigroup/Group proof

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

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

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

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

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

intros.
exists right_unit.

intro.

destruct (right_inverse u).
exists x.

assumption.
Qed.

Accessing Ackermann

(* The Ackermann function is defined by the equations:
 *
 *          n+1             m=0
 * A(m,n) = A(m-1,1)        m>0 n=0
 *          A(m-1,A(m,n-1)) m>0 n>0
 *)

(* It's an example of something not structurally recursive,
 * that means it's going to be a lot of fun to try and define
 * in type theory.
 *)

(* A simple example to look at first is double: *)
Fixpoint double (n : nat) : nat :=
  match n with
    | O => O
    | S m => S (S (double m))
  end.

(* From the definition you can see that every application of double
 * is done with m = S n
 *)

Definition nat_struct n m := m = S n.

(* This is a well founded relation *)

Theorem well_founded_nat_struct : well_founded nat_struct.
  unfold well_founded.
  (* forall a : nat, Acc nat_struct a *)
  Print Acc.
  (* Inductive Acc (A : Type) (R : A -> A -> Prop) (x : A) : Prop :=
         Acc_intro : (forall y : A, R y x -> Acc R y) -> Acc R x
   *)
  (* For some relation to be well founded, every element must be
     accessable
   *)
  induction a.
  (*
     ============================
     Acc nat_struct 0
     
     subgoal 2 is:
     Acc nat_struct (S a)
   *)
  apply Acc_intro; intros.
  discriminate.
  
  apply Acc_intro; intros.
  injection H; intros.
  (*
     a : nat
     IHa : Acc nat_struct a
     y : nat
     H : nat_struct y (S a)
     H0 : a = y
     ============================
     Acc nat_struct y
   *)
  rewrite <- H0; assumption.
Defined.
(* Must used Defined. instead of Qed. here if you want to be
 * able to use the computational properties of any definition
 * given by well_founded_induction on nat_struct
 *)

Definition double' : nat -> nat.
apply (well_founded_induction well_founded_nat_struct).
(*  ============================
   forall x : nat, (forall y : nat, nat_struct y x -> nat) -> nat
 *)
intros x double'.
refine (match x as x' return x = x' -> nat
             (* the trick here ^ is one of many that gives me more
                information about the pattern match than I would get
                normally *)
          with
          | O => fun eq => O
          | S n => fun eq => S (S (double' n _))
                      (* the underscore here ^ is a proof obligation *)
        end (refl_equal x)).
(* x : nat
   double' : forall y : nat, nat_struct y x -> nat
   n : nat
   eq : x = S n
   ============================
   nat_struct n x
*)
unfold nat_struct.
(* x : nat
   double' : forall y : nat, nat_struct y x -> nat
   n : nat
   eq : x = S n
   ============================
   x = S n
 *)
congruence.
Defined.

Print double'.
(*
double' = 
well_founded_induction well_founded_nat_struct (fun _ : nat => nat)
  (fun (x : nat) (double' : forall y : nat, nat_struct y x -> nat) =>
   match x as x' return (x = x' -> nat) with
   | 0 => fun _ : x = 0 => 0
   | S n => fun eq : x = S n => S (S (double' n eq))
   end (refl_equal x))
     : nat -> nat
*)

Eval compute in (double' 6).
(*     = 12
       : nat *)

Extraction double'.
(* let rec double' = function
 *   | O -> O
 *   | S n -> S (S (double' n))
 *)

(* The extraction is very very clean, which is excellent!
 * It's just that one would like to know -why- the extraction
 * doesn't have any 'Acc' or 'well_founded_induction' in it.
 * It's not to do with Prop vs Set or Defined/Qed, the reason is
 *
 * Coq/contrib/extraction/mlutil.ml:

let manual_inline_list = 
  let mp = MPfile (dirpath_of_string "Coq.Init.Wf") in 
  List.map (fun s -> (make_con mp empty_dirpath (mk_label s)))
    [ "well_founded_induction_type"; "well_founded_induction"; 
      "Acc_rect"; "Acc_rec" ; "Acc_iter" ; "Fix" ]
 
 *
 * I wish I knew why this was in here, I can only assume it's
 * some kind of historical artifact, anyway,

Extraction Inline foo bar baz.
 
 * works fine if I were to defined my own Acc type thing.
 *)


(* So now we know _what_ to do, it's just a simple matter of doing it
 * I must define a relation that is Well Founded (and prove that),
 * and is suitable for defining the Ackermann function with
 *)

Definition lt_prod_lt : nat * nat -> nat * nat -> Prop :=
  fun pq mn =>
    let (p,q) := pq in
    let (m,n) := mn in
         p < m
      \/ p = m /\ q < n.

Require Import Omega.

Theorem well_founded_lt_prod_lt : well_founded lt_prod_lt.
  (* ... long ugly proof omitted ... *)
Defined.

Definition Ackermann : nat -> nat -> nat.
intros m n; generalize (m,n); clear m n. (* currying *)
apply (well_founded_induction well_founded_lt_prod_lt).
destruct x as (m,n).
intro Ackermann.
refine
  (match m as m', n as n' return m = m' -> n = n' -> nat with
     | 0,   n   => fun _ _ => S n
     | S m, 0   => fun eq eq' => Ackermann (m, 1) _
     | S m, S n => fun eq eq' => let x := Ackermann (S m, n) _ in Ackermann (m, x) _
   end (refl_equal m) (refl_equal n));
  rewrite eq; rewrite eq'; unfold lt_prod_lt; auto with arith.
Defined.

Eval vm_compute in (Ackermann 3 4).
(*     = 125
 *     : nat *)

Extraction Ackermann.
(*
let ackermann m n =
  let rec f = function
    | Pair (m0, n0) ->
        (match m0 with
           | O -> S n0
           | S m1 ->
               (match n0 with
                  | O -> f (Pair (m1, (S O)))
                  | S n1 -> f (Pair (m1, (f (Pair ((S m1), n1)))))))
  in f (Pair (m, n))
*)

(* Lots of fabulous tupling and untupling,
 * Actually, I don't like that, so I have defined a curried
 * Acc2 and given similar definitions as the Wf does
 *)

Require Import Acc2.

Definition lexi : nat -> nat ->
                  nat -> nat ->
                  Prop :=
  fun p q m n =>
       p < m
    \/ p = m /\ q < n.

Theorem well_founded2_lexi : well_founded2 lexi.
  unfold well_founded2; unfold lexi.
  induction m.
   induction n.
    apply Acc2_intro; intros.
     elimtype False; omega.
    apply Acc2_intro; intros.
    destruct H.
     inversion H.
     destruct H.
     destruct (lt_eq_lt_dec q n). destruct s.
      destruct IHn.
      apply H1.
      right; split; auto.
      rewrite H; rewrite e; apply IHn.
      elimtype False; omega.
   induction n.
    apply Acc2_intro; intros.
    destruct H.
     apply Acc2_intro; intros.
     destruct H0.
      destruct (IHm q).
      apply H1.
       left; omega.
      destruct H0.
      rewrite H0.
      destruct (IHm q).
      apply H2.
      destruct (lt_eq_lt_dec p m). destruct s.
       left; assumption.
       right; split; assumption.
       elimtype False; omega.
      destruct H.
      inversion H0.
     apply Acc2_intro; intros.
     destruct H.
      destruct IHn.
      apply H0.
      left; assumption.
     destruct H.
     destruct (lt_eq_lt_dec q n). destruct s.
      rewrite H.
       destruct IHn.
       apply H1.
       right; split; auto.
      rewrite H; rewrite e; apply IHn.
      elimtype False; omega.
Defined.

Definition Ack2 : nat -> nat -> nat.
apply (well_founded2_induction well_founded2_lexi); intros m n Ack2.
refine
  (match m as m', n as n' return m = m' -> n = n' -> nat with
     | 0,   n   => fun eq eq' => S n
     | S m, 0   => fun eq eq' => Ack2 m 1 _
     | S m, S n => fun eq eq' => let x := Ack2 (S m) n _
                                  in Ack2 m x _
   end (refl_equal m) (refl_equal n));
  unfold lexi; rewrite eq; rewrite eq'.
left; auto.
right; auto.
left; auto.
Defined.

(* One thing I don't like, is having this let x := .. but I don't know
 * how to remove that yet, anyway it doesn't matter much
 *)

Extraction Ack2.
(*
let rec ack2 m n =
  match m with
    | O -> S n
    | S m0 ->
        (match n with
           | O -> ack2 m0 (S O)
           | S n0 -> ack2 m0 (ack2 (S m0) n0))
*)
Extraction Language Haskell.
Extraction Ack2.
(*
ack2 :: Nat -> Nat -> Nat
ack2 m n =
  case m of
    O -> S n
    S m0 -> (case n of
               O -> ack2 m0 (S O)
               S n0 -> ack2 m0 (ack2 (S m0) n0))
*)

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.