Require Import Coq.Init.Nat.
Require Import Coq.Strings.String.
Require Import Coq.Vectors.VectorDef.

Open Scope string_scope.
Open Scope nat_scope.


(* Traversal definition and methods *)

Record result T A B := mkResult
{ n : nat
; apply : (t A n) * (t B n -> T)
}.
Arguments mkResult [T A B].
Arguments n [T A B].
Arguments apply [T A B].

Definition traversal S T A B := S -> result T A B.

Definition getAll {S T A B} (tr : traversal S T A B) (s : S) : t A (n (tr s)) :=
  fst (apply (tr s)).

Definition putAll {S T A B} (tr : traversal S T A B) (s : S) : (t B (n (tr s))) -> T :=
  snd (apply (tr s)).


(* Examples *)

Inductive person : Type :=
 | mkPerson : string -> string -> nat -> person.

Definition nameTr : traversal person person string string := (fun s =>
  match s with
  | mkPerson first last age => mkResult _
      (cons _ first _ (cons _ last _ (nil _)),
       fun bs => mkPerson (hd bs) (hd (tl bs)) (age))
  end).

Example get_names :
  getAll nameTr (mkPerson "john" "doe" 40) =
  cons string "john" 1 (cons string "doe" 0 (nil string)).
Proof. auto. Qed.

Example put_names :
  putAll nameTr (mkPerson "john" "doe" 40) (cons _ "jane" _ (cons _ "roe" _ (nil _))) =
  mkPerson "jane" "roe" 40.
Proof. auto. Qed.

Definition vectorTr {A B n} : traversal (t A n) (t B n) A B :=
  fun s => mkResult _ (s, id).

Example get_as : forall B,
  @getAll _ _ _ B vectorTr (cons _ 1 _ (cons _ 2 _ (nil _))) =
  cons _ 1 _ (cons _ 2 _ (nil _)).
Proof. auto. Qed.

Example set_bs :
  putAll vectorTr (cons _ 1 _ (cons _ 2 _ (nil _))) (cons _ "a" _ (cons _ "b" _ (nil _))) =
  (cons _ "a" _ (cons _ "b" _ (nil _))).
Proof. auto. Qed.

Inductive tree (A : Type) : nat -> Type :=
  | leaf : tree A 0
  | node {m} : tree A m -> A -> tree A m -> tree A (S m).

Require Import ZArith.

Example xyz : forall n, pred (2 ^ n) + S (pred (2 ^ n)) = pred (2 ^ S n).
Proof.
  intros.
  rewrite Nat.succ_pred.
  - admit.
  - assert (G : forall o p, (exists m n, (o = S m) \/ (p = S n)) -> o + p <> 0).
    { admit.
    }
    destruct n0; simpl; auto.
    rewrite <- plus_n_O.
    apply G.
    induction n0; simpl.
    + exists 0, 0. now left.
    + rewrite <- plus_n_O.
      destruct IHn0, H, H.
      * exists x, x0.
Admitted.

Fixpoint inorder {A m} (tr : tree A m) : t A (pred (2 ^ m)) :=
  match tr with
  | leaf _ => nil _
  | node _ l a r => append (inorder l) (cons _ a _ (inorder r))
  end.

Example inorderTr {A B m} : traversal (tree A m) (tree B m) A B := fun s =>
  match s with
  | leaf _ => mkResult 0 (nil A, fun _ => leaf B)
  | node l a r => mkResult _ (inorder (node l a r), )
  end.

(* Doesn't compile! (which is fine) *)

(*
Example put_names :
  putAll nameTr (mkPerson "john" "doe" 40) (cons _ "jane" _ (nil _)) =
  mkPerson "jane" "roe" 40.

Example get_names' :
  getAll nameTr (mkPerson "john" "doe" 40) =
  (cons string "john" 0 (nil string)).
*)