From Equations Require Import Equations.
Require Import Equations.Subterm.
Require Import Lia.

Section Tests.

  Variable A : Type.

  Inductive forest : Type :=
  | emp : A -> forest
  | tree : list forest -> forest.

  Equations fweight (f : forest) : nat :=
    {
      fweight emp := 1;
      fweight (tree l) := 1 + lweight l
    }
  where lweight (l : list forest) : nat :=
    {
      lweight nil := 1;
      lweight (cons f l') := fweight f + lweight l'
    }.


  Fail Equations flatten (f : forest) : list A :=
    {
      flatten f by rec (fweight f) lt :=
      flatten emp := nil;
      flatten (tree l) := lflatten l
    }
  where lflatten (l : list forest) : list A :=
    {
      lflatten nil := nil;
      lflatten (cons f l') := flatten f ++ lflatten l'
    }.
  (* The command has indeed failed with message: *)
  (* The variable lflatten was not found in the current environment. *)

  Inductive tail_of {A} : list A -> list A -> Prop :=
  | t_refl : forall l, tail_of l l
  | t_cons : forall x l1 l2, tail_of l1 l2 -> tail_of l1 (cons x l2).
  Hint Constructors tail_of.

  Lemma tail_of_decons : forall {A} {x : A} {l1 l2},
      tail_of (cons x l1) l2 ->
      tail_of l1 l2.
  Proof.
    intros. remember (cons x l1) as l.
    revert Heql. revert l1.
    induction H; intros; subst; auto.
  Qed.

  Lemma fweight_neq_0 : forall f, fweight f <> 0.
  Proof.
    intros.
    destruct f.
    Fail funelim (fweight (emp a)).

    Restart.

    intros. destruct f; simp fweight; lia.
  Qed.

  Lemma lweight_neq_0 : forall l, lweight l <> 0.
  Proof.
    intros. destruct l; simpl.
    lia.
    pose proof (fweight_neq_0 f). lia.
  Qed.

  Lemma tail_of_fweight : forall l1 l2,
      tail_of l1 l2 ->
      lweight l1 <= lweight l2.
  Proof.
    induction 1; simp lweight; try lia.
    simpl. pose proof (fweight_neq_0 x).
    lia.
  Qed.

  Equations flatten (f : forest) : list A :=
    {
      flatten f by rec (fweight f) lt :=
      flatten emp := nil;
      flatten (tree l) :=
        let fix func (fs : list forest) (t : tail_of fs l) : list A :=
            match fs as fs0 return tail_of fs0 l -> list A with
            | nil => fun _ => nil
            | cons f fs' =>
              fun t' => app (flatten f) (func fs' (tail_of_decons t'))
            end t in
        func l (t_refl _)
    }.
  Next Obligation.
    apply tail_of_fweight in t'.
    simpl in t'.
    pose proof (lweight_neq_0 fs').
    simp fweight. lia.
  Fail Qed.

(* flatten_obligation_1 is defined *)
(* No more obligations remaining *)
(* The command has indeed failed with message: *)
(* Recursive definition of func is ill-formed. *)
(* In environment *)
(* A : Type *)
(* f : forest *)
(* hypspack := {| pr1 := f; pr2 := () |} : sigma forest (fun _ : forest => ()) *)
(* pack := fweight f : nat *)
(* hypspack0 : sigma forest (fun _ : forest => ()) *)
(* _tmp := fweight (pr1 hypspack0) : nat *)
(* H : sigma forest (fun _ : forest => ()) *)
(* X : *)
(* forall y : sigma forest (fun _ : forest => ()), *)
(* MR lt (fun hypspack : sigma forest (fun _ : forest => ()) => fweight (pr1 hypspack)) y H -> list A *)
(* f0 : forest *)
(* H0 : () *)
(* flatten : *)
(* forall y : sigma forest (fun _ : forest => ()), *)
(* fweight (pr1 y) < fweight (pr1 {| pr1 := f0; pr2 := H0 |}) -> list A *)
(* flatten0 := fun f : forest => flatten {| pr1 := f; pr2 := () |} : *)
(* forall f : forest, fweight (pr1 {| pr1 := f; pr2 := () |}) < fweight f0 -> list A *)
(* f1 : forest *)
(* flatten1 : forall f : forest, fweight f < fweight f1 -> list A *)
(* l : list forest *)
(* flatten2 : forall f : forest, fweight f < fweight (tree l) -> list A *)
(* func : forall fs : list forest, tail_of fs l -> list A *)
(* fs : list forest *)
(* t : tail_of fs l *)
(* f2 : forest *)
(* fs' : list forest *)
(* t' : tail_of (f2 :: fs') l *)
(* Recursive call to func has not enough arguments. *)
(* Recursive definition is: *)
(* "fun (fs : list forest) (t : tail_of fs l) => *)
(*  match fs as fs0 return (tail_of fs0 l -> list A) with *)
(*  | []%list => fun _ : tail_of [] l => []%list *)
(*  | (f :: fs')%list => *)
(*      fun t' : tail_of (f :: fs') l => *)
(*      (flatten_comp_proj f (flatten2 f (flatten_obligation_1 l flatten2 func fs t f fs' t')) ++ *)
(*       func fs' (tail_of_decons t'))%list *)
(*  end t". *)

End Tests.