fast_beq.v

Require Import Coq.Lists.List.
Require Import Coq.Bool.Bool.
Import ListNotations.

Variant t := | a0 | a1.
Variant t2 : Type :=
| b0
| b1 `(t) `(t) `(t)
| b2 `(t)
| b3 `(t)
| b4 `(t)
| b5 `(t)
| b6 `(t)
| b7 `(t)
| b8 `(t)
| b9 `(t)
| b10 `(t)
| b11 `(t)
| b12 `(t)
| b13 `(t)
| b14 `(t)
| b15 `(t)
| b16 `(t)
| b17 `(t)
| b18 `(t)
| b19 `(t)
| b20 `(t)
| b21 `(t)
| b22 `(t)
| b23 `(t)
| b24 `(t)
| b25 `(t)
| b26 `(t)
| b27 `(t)
| b28 `(t)
| b29 `(t)
| b30 `(t)
| b31 `(t)
| b32 `(t)
| b33 `(t)
| b34 `(t)
| b35 `(t)
| b36 `(t)
| b37 `(t)
| b38 `(t)
| b39 `(t)
| b40 `(t)
| b41 `(t)
| b42 `(t)
| b43 `(t)
| b44 `(t)
| b45 `(t)
| b46 `(t)
| b47 `(t)
| b48 `(t)
| b49 `(t)
| b50 `(t)
| b51 `(t)
| b52 `(t)
| b53 `(t)
| b54 `(t)
| b55 `(t)
| b56 `(t)
| b57 `(t)
| b58 `(t)
| b59 `(t)
| b60 `(t)
| b61 `(t)
| b62 `(t)
| b63 `(t)
| b64 `(t)
| b65 `(t)
| b66 `(t)
| b67 `(t)
| b68 `(t)
| b69 `(t)
| b70 `(t).

Record eqtype (A : Type) := {
  beq : A -> A -> bool;
  reflect_beq : forall x y, reflect (x = y) (beq x y)
}.

Fixpoint expand (l : list Type) t : Type :=
  match l with
  | [] => t
  | t1 :: l => t1 -> expand l t
  end.

Record constr_descr (T : Type) := {
  types : list {A & eqtype A & T -> A};
  constructor : expand (map (fun t => projT1 (sigT_of_sigT2 t)) types) T
}.

Definition B0 : constr_descr t2 := {|
  types := [];
  constructor := b0
|}.

Scheme Equality for t.
Lemma reflect_t_beq : forall x y, reflect (x = y) (t_beq x y).
Proof.
  intros. destruct (t_beq x y) eqn:heq; constructor.
  - apply internal_t_dec_bl. assumption.
  - intros contra. apply not_true_iff_false in heq. contradiction heq.
    apply internal_t_dec_lb. assumption.
Qed.

Definition t_eqtype : eqtype t := {|
  beq := t_beq;
  reflect_beq := reflect_t_beq
|}.

Definition B1 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _;
            existT2 _ _ (t:Type) t_eqtype _;
            existT2 _ _ (t:Type) t_eqtype _];
  constructor := b1
|}.
- intros x. destruct x. 2:apply H. all: exact a0. (* default value *)
- intros x. destruct x. 2:apply H0. all: exact a0. (* default value *)
- intros x. destruct x. 2:apply H1. all: exact a0. (* default value *)
Defined.

Definition B2 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b2
|}.
intros x. destruct x. 3:assumption. all: exact a0. (* default value *)
Defined.

Definition B3 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b3
|}.
intros x. destruct x. 4:assumption. all: exact a0. (* default value *)
Defined.

Definition B4 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b4
|}.
intros x. destruct x. 5:assumption. all: exact a0. (* default value *)
Defined.

Definition B5 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b5
|}.
intros x. destruct x. 6:assumption. all: exact a0. (* default value *)
Defined.

Definition B6 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b6
|}.
intros x. destruct x. 7:assumption. all: exact a0. (* default value *)
Defined.

Definition B7 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b7
|}.
intros x. destruct x. 8:assumption. all: exact a0. (* default value *)
Defined.

Definition B8 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b8
|}.
intros x. destruct x. 9:assumption. all: exact a0. (* default value *)
Defined.

Definition B9 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b9
|}.
intros x. destruct x. 10:assumption. all: exact a0. (* default value *)
Defined.

Definition B10 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b10
|}.
intros x. destruct x. 11:assumption. all: exact a0. (* default value *)
Defined.

Definition B11 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b11
|}.
intros x. destruct x. 12:assumption. all: exact a0. (* default value *)
Defined.

Definition B12 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b12
|}.
intros x. destruct x. 13:assumption. all: exact a0. (* default value *)
Defined.

Definition B13 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b13
|}.
intros x. destruct x. 14:assumption. all: exact a0. (* default value *)
Defined.

Definition B14 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b14
|}.
intros x. destruct x. 15:assumption. all: exact a0. (* default value *)
Defined.

Definition B15 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b15
|}.
intros x. destruct x. 16:assumption. all: exact a0. (* default value *)
Defined.

Definition B16 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b16
|}.
intros x. destruct x. 17:assumption. all: exact a0. (* default value *)
Defined.

Definition B17 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b17
|}.
intros x. destruct x. 18:assumption. all: exact a0. (* default value *)
Defined.

Definition B18 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b18
|}.
intros x. destruct x. 19:assumption. all: exact a0. (* default value *)
Defined.

Definition B19 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b19
|}.
intros x. destruct x. 20:assumption. all: exact a0. (* default value *)
Defined.

Definition B20 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b20
|}.
intros x. destruct x. 21:assumption. all: exact a0. (* default value *)
Defined.

Definition B21 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b21
|}.
intros x. destruct x. 22:assumption. all: exact a0. (* default value *)
Defined.

Definition B22 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b22
|}.
intros x. destruct x. 23:assumption. all: exact a0. (* default value *)
Defined.

Definition B23 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b23
|}.
intros x. destruct x. 24:assumption. all: exact a0. (* default value *)
Defined.

Definition B24 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b24
|}.
intros x. destruct x. 25:assumption. all: exact a0. (* default value *)
Defined.

Definition B25 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b25
|}.
intros x. destruct x. 26:assumption. all: exact a0. (* default value *)
Defined.

Definition B26 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b26
|}.
intros x. destruct x. 27:assumption. all: exact a0. (* default value *)
Defined.

Definition B27 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b27
|}.
intros x. destruct x. 28:assumption. all: exact a0. (* default value *)
Defined.

Definition B28 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b28
|}.
intros x. destruct x. 29:assumption. all: exact a0. (* default value *)
Defined.

Definition B29 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b29
|}.
intros x. destruct x. 30:assumption. all: exact a0. (* default value *)
Defined.

Definition B30 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b30
|}.
intros x. destruct x. 31:assumption. all: exact a0. (* default value *)
Defined.

Definition B31 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b31
|}.
intros x. destruct x. 32:assumption. all: exact a0. (* default value *)
Defined.

Definition B32 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b32
|}.
intros x. destruct x. 33:assumption. all: exact a0. (* default value *)
Defined.

Definition B33 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b33
|}.
intros x. destruct x. 34:assumption. all: exact a0. (* default value *)
Defined.

Definition B34 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b34
|}.
intros x. destruct x. 35:assumption. all: exact a0. (* default value *)
Defined.

Definition B35 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b35
|}.
intros x. destruct x. 36:assumption. all: exact a0. (* default value *)
Defined.

Definition B36 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b36
|}.
intros x. destruct x. 37:assumption. all: exact a0. (* default value *)
Defined.

Definition B37 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b37
|}.
intros x. destruct x. 38:assumption. all: exact a0. (* default value *)
Defined.

Definition B38 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b38
|}.
intros x. destruct x. 39:assumption. all: exact a0. (* default value *)
Defined.

Definition B39 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b39
|}.
intros x. destruct x. 40:assumption. all: exact a0. (* default value *)
Defined.

Definition B40 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b40
|}.
intros x. destruct x. 41:assumption. all: exact a0. (* default value *)
Defined.

Definition B41 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b41
|}.
intros x. destruct x. 42:assumption. all: exact a0. (* default value *)
Defined.

Definition B42 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b42
|}.
intros x. destruct x. 43:assumption. all: exact a0. (* default value *)
Defined.

Definition B43 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b43
|}.
intros x. destruct x. 44:assumption. all: exact a0. (* default value *)
Defined.

Definition B44 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b44
|}.
intros x. destruct x. 45:assumption. all: exact a0. (* default value *)
Defined.

Definition B45 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b45
|}.
intros x. destruct x. 46:assumption. all: exact a0. (* default value *)
Defined.

Definition B46 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b46
|}.
intros x. destruct x. 47:assumption. all: exact a0. (* default value *)
Defined.

Definition B47 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b47
|}.
intros x. destruct x. 48:assumption. all: exact a0. (* default value *)
Defined.

Definition B48 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b48
|}.
intros x. destruct x. 49:assumption. all: exact a0. (* default value *)
Defined.

Definition B49 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b49
|}.
intros x. destruct x. 50:assumption. all: exact a0. (* default value *)
Defined.

Definition B50 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b50
|}.
intros x. destruct x. 51:assumption. all: exact a0. (* default value *)
Defined.

Definition B51 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b51
|}.
intros x. destruct x. 52:assumption. all: exact a0. (* default value *)
Defined.

Definition B52 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b52
|}.
intros x. destruct x. 53:assumption. all: exact a0. (* default value *)
Defined.

Definition B53 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b53
|}.
intros x. destruct x. 54:assumption. all: exact a0. (* default value *)
Defined.

Definition B54 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b54
|}.
intros x. destruct x. 55:assumption. all: exact a0. (* default value *)
Defined.

Definition B55 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b55
|}.
intros x. destruct x. 56:assumption. all: exact a0. (* default value *)
Defined.

Definition B56 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b56
|}.
intros x. destruct x. 57:assumption. all: exact a0. (* default value *)
Defined.

Definition B57 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b57
|}.
intros x. destruct x. 58:assumption. all: exact a0. (* default value *)
Defined.

Definition B58 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b58
|}.
intros x. destruct x. 59:assumption. all: exact a0. (* default value *)
Defined.

Definition B59 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b59
|}.
intros x. destruct x. 60:assumption. all: exact a0. (* default value *)
Defined.

Definition B60 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b60
|}.
intros x. destruct x. 61:assumption. all: exact a0. (* default value *)
Defined.

Definition B61 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b61
|}.
intros x. destruct x. 62:assumption. all: exact a0. (* default value *)
Defined.

Definition B62 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b62
|}.
intros x. destruct x. 63:assumption. all: exact a0. (* default value *)
Defined.

Definition B63 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b63
|}.
intros x. destruct x. 64:assumption. all: exact a0. (* default value *)
Defined.

Definition B64 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b64
|}.
intros x. destruct x. 65:assumption. all: exact a0. (* default value *)
Defined.

Definition B65 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b65
|}.
intros x. destruct x. 66:assumption. all: exact a0. (* default value *)
Defined.

Definition B66 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b66
|}.
intros x. destruct x. 67:assumption. all: exact a0. (* default value *)
Defined.

Definition B67 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b67
|}.
intros x. destruct x. 68:assumption. all: exact a0. (* default value *)
Defined.

Definition B68 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b68
|}.
intros x. destruct x. 69:assumption. all: exact a0. (* default value *)
Defined.

Definition B69 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b69
|}.
intros x. destruct x. 70:assumption. all: exact a0. (* default value *)
Defined.

Definition B70 : constr_descr t2. refine {|
  types := [existT2 _ _ (t:Type) t_eqtype _];
  constructor := b70
|}.
intros x. destruct x. 71:assumption. all: exact a0. (* default value *)
Defined.

Definition ls : list (constr_descr t2) := [
B0;
B1;
B2;
B3;
B4;
B5;
B6;
B7;
B8;
B9;
B10;
B11;
B12;
B13;
B14;
B15;
B16;
B17;
B18;
B19;
B20;
B21;
B22;
B23;
B24;
B25;
B26;
B27;
B28;
B29;
B30;
B31;
B32;
B33;
B34;
B35;
B36;
B37;
B38;
B39;
B40;
B41;
B42;
B43;
B44;
B45;
B46;
B47;
B48;
B49;
B50;
B51;
B52;
B53;
B54;
B55;
B56;
B57;
B58;
B59;
B60;
B61;
B62;
B63;
B64;
B65;
B66;
B67;
B68;
B69;
B70
].

Section fin.
  Context (t: Type)
          (ls : list (constr_descr t))
          (to_nat : t -> nat).
(*
  Fixpoint forallbi {A} (f : nat -> A -> bool) (l : list A) :=
    match l with
    | [] => true
    | a :: l => f 0 a && forallbi (fun n => f (S n)) l
    end.
*)
  Definition beq_gen (x y : t) :=
    let n_x := to_nat x in
    let n_y := to_nat y in
    if Nat.eqb n_x n_y then
      match nth_error ls n_x with
      | None => false (* unreachable *)
      | Some c => forallb (fun (c:{A & eqtype A & t -> A}) =>
        let A := projT1 (sigT_of_sigT2 c) in
        let beq : A -> A -> bool := beq _ (projT2 (sigT_of_sigT2 c)) in
        let arg : t -> A := projT3 c in
        beq (arg x) (arg y)) c.(types _)
      end
    else false.

  Definition eval (l : list {A : Type & eqtype A & t -> A}) (c : expand (map (fun t => projT1 (sigT_of_sigT2 t)) l) t) (x:t) : t.
  Proof.
    revert l c x.
    fix eval 1. intros. destruct l. simpl in c. apply c.
    simpl in c.
    set (d := c (projT3 s x)).
    apply (eval l d x).
  Defined.

  Context (ls_has_all : forall e,
    match nth_error ls (to_nat e) with
    | Some c => eval (types _ c) (constructor _ c) e = e
    | None => False
    end).

Lemma nth_error_beq x y : beq_gen x y = true -> x = y.
Proof.
  unfold beq_gen. destruct (PeanoNat.Nat.eqb_spec (to_nat x) (to_nat y)); [|discriminate].
  destruct nth_error as [c|] eqn:heq; [|discriminate].
  pose proof (ls_has_all x) as H1. rewrite heq in H1.
  pose proof (ls_has_all y) as H2. rewrite <- e, heq in H2.
  pattern x at 2.
  rewrite <- H1.
  pattern y at 2.
  rewrite <- H2. clear H1 H2 heq e.
  generalize (constructor t c) x y.
  induction (types t c).
  - simpl. reflexivity.
  - simpl. destruct a as [A EQ proj]. simpl.
    intros ???. rewrite andb_true_iff. intros [heq H].
    assert (proj x0 = proj y0) as Ha.
    { destruct (reflect_beq _ EQ (proj x0) (proj y0)).
      assumption. discriminate.
    }
    apply IHl with (e:=e (proj x0)) in H.
    rewrite <- Ha. assumption.
Qed.

Lemma reflect_of_fin : forall x y, reflect (x = y) (beq_gen x y).
Proof.
  intros x y; remember (beq_gen x y) as b eqn:Heqb; destruct b; symmetry in Heqb; constructor.
  { apply nth_error_beq. assumption. }
  { intro H; subst y.
    revert Heqb. unfold beq_gen.
    rewrite PeanoNat.Nat.eqb_refl.
    specialize (ls_has_all x). destruct nth_error as [c|]; [|contradiction].
    clear ls_has_all.
    induction (types t c).
    - simpl. discriminate.
    - destruct a as [A EQ proj]. simpl.
      rewrite andb_false_iff.
      intros [H|H].
      destruct (reflect_beq _ EQ (proj x) (proj x)). discriminate. contradiction.
      apply IHl. assumption.
  }
Qed.

End fin.

Definition to_nat x :=
  match x with
| b0 => 0
| b1 _ _ _ => 1
| b2 _ => 2
| b3 _ => 3
| b4 _ => 4
| b5 _ => 5
| b6 _ => 6
| b7 _ => 7
| b8 _ => 8
| b9 _ => 9
| b10 _ => 10
| b11 _ => 11
| b12 _ => 12
| b13 _ => 13
| b14 _ => 14
| b15 _ => 15
| b16 _ => 16
| b17 _ => 17
| b18 _ => 18
| b19 _ => 19
| b20 _ => 20
| b21 _ => 21
| b22 _ => 22
| b23 _ => 23
| b24 _ => 24
| b25 _ => 25
| b26 _ => 26
| b27 _ => 27
| b28 _ => 28
| b29 _ => 29
| b30 _ => 30
| b31 _ => 31
| b32 _ => 32
| b33 _ => 33
| b34 _ => 34
| b35 _ => 35
| b36 _ => 36
| b37 _ => 37
| b38 _ => 38
| b39 _ => 39
| b40 _ => 40
| b41 _ => 41
| b42 _ => 42
| b43 _ => 43
| b44 _ => 44
| b45 _ => 45
| b46 _ => 46
| b47 _ => 47
| b48 _ => 48
| b49 _ => 49
| b50 _ => 50
| b51 _ => 51
| b52 _ => 52
| b53 _ => 53
| b54 _ => 54
| b55 _ => 55
| b56 _ => 56
| b57 _ => 57
| b58 _ => 58
| b59 _ => 59
| b60 _ => 60
| b61 _ => 61
| b62 _ => 62
| b63 _ => 63
| b64 _ => 64
| b65 _ => 65
| b66 _ => 66
| b67 _ => 67
| b68 _ => 68
| b69 _ => 69
| b70 _ => 70
  end.

Lemma ls_has_all : forall e,
    match nth_error ls (to_nat e) with
    | Some c => eval t2 (types _ c) (constructor _ c) e = e
    | None => False
    end.
Proof. destruct e; reflexivity. Qed.

Definition t2_beq := beq_gen _ ls to_nat.

Lemma reflect_t2_beq : forall x y, reflect (x = y) (t2_beq x y).
Proof. apply reflect_of_fin. apply ls_has_all. Qed.

fast_beq_nice.v

Require Import List. Import ListNotations.
Require Import Arith.
From mathcomp Require Import all_ssreflect.

Inductive t := a0 | a1.

Inductive t2 :=
| b0 : t2
| b1 : nat -> t2
| b2 : bool -> t2.

Definition type_constr n : list eqType :=
  match n with
  | 0 => []
  | 1 => [nat_eqType]
  | 2 => [bool_eqType]
  | _ => []
  end.

Inductive hlist : list eqType -> Type :=
| hnil : hlist []
| hcons : forall {A:eqType} {l:seq eqType}, A -> hlist l -> hlist (A::l).

Definition proj (x:t2) :
  {n : nat & hlist (type_constr n) } :=
  match x with
  | b0 => existT _ 0 hnil
  | b1 n => existT _ 1 (hcons n hnil)
  | b2 x => existT _ 2 (hcons x hnil)
  end.

Fixpoint expand (l : list Type) t : Type :=
  match l with
  | [] => t
  | t1 :: l => t1 -> expand l t
  end.

Definition constructor (n:nat) : expand (List.map Equality.sort (type_constr n)) t2 :=
  match n with
  | 0 => b0
  | 1 => b1
  | 2 => b2
  | _ => b0 (* what if there is no default value? *)
  end.

Fixpoint eval {lT A} (l : hlist lT) : expand (map Equality.sort lT) A -> A :=
  match l with
  | hnil => fun x => x
  | hcons _ _ a l => fun x => eval l (x a)
  end.

Definition reconstruct x :=
  let 'existT n l := proj x in
  let c := constructor n in
  eval l c.

Lemma reconstruct_correct : forall x, reconstruct x = x.
Proof.
  destruct x; reflexivity.
Qed.

Fixpoint hforall2 {lT} (l1 : hlist lT) : hlist lT -> bool.
refine (
  match l1 with
  | hnil =>
    fun l2 => match l2 with
              | hnil => true
              | hcons _ _ _ _ => false
              end
  | hcons A lT x1 l1 =>
    fun l2 =>
      match l2 in hlist l return l = A :: lT -> bool with
      | hnil => fun _ => false (* impossible case *)
      | hcons _ _ x2 l2 => _ (* fun H => _ && hforall2 l1 l2 *)
      end erefl
  end).
  intros. inversion H; subst.
  apply andb.
  apply (x1 == x2).
  apply (hforall2 _ l1 l2).
Defined.

Definition t2_eqb x y :=
  let 'existT xi xA := proj x in
  let 'existT yi yA := proj y in
  match Nat.eq_dec xi yi with
  | left H => hforall2 (ecast k (hlist (type_constr k)) H xA) yA
  | right _ => false
  end.

From Equations Require Import Equations.
Lemma hforall2_correct {lT A} (xA yA:hlist lT) c :
  hforall2 xA yA = true -> @eval _ A xA c = eval yA c.
Proof.
  induction xA.
  dependent elimination yA. reflexivity.
  dependent elimination yA => /=.
  move=> /andP [/eqP <- /IHxA <-].
  done.
Qed.

Lemma t2_eqb_correct x y : t2_eqb x y -> reconstruct x = reconstruct y.
Proof.
  rewrite /t2_eqb /reconstruct.
  case: (proj x) => xi xA.
  case: (proj y) => yi yA.
  case: Nat.eq_dec => heq //.
  destruct heq. (* how to do that in ssreflect ? *)
  move=> /hforall2_correct <-. reflexivity.
Qed.

Lemma hforall2_refl {lT} (xA : hlist lT) :
  hforall2 xA xA.
Proof.
  induction xA.
  done.
  simpl. by apply /andP.
Qed.

Lemma t2_eqb_reflect x y : reflect (x = y) (t2_eqb x y).
Proof.
  apply (iffP idP).
  + move=> /t2_eqb_correct. by rewrite !reconstruct_correct.
  move=> <-.
  rewrite /t2_eqb.
  case: (proj x) => xi xA.
  case: Nat.eq_dec => //.
  intros a.
  rewrite (Eqdep_dec.UIP_refl_nat _ a).
  by apply hforall2_refl.
Qed.

fast_beq_recursive.v

Require Import Coq.Lists.List.
Require Import Coq.Bool.Bool.
Import ListNotations.

Variant t := | a0 | a1.
Inductive t2 : Type :=
| b0
| b1 `(t) `(t) `(t)
| b2 `(t) `(t2)
| b3 `(nat)
| b4 `(bool)
| b5 `(t)
| b6 `(t)
| b7 `(t)
| b8 `(t)
| b9 `(t)
| b10 `(t)
| b11 `(t)
| b12 `(t)
| b13 `(t)
| b14 `(t)
| b15 `(t)
| b16 `(t)
| b17 `(t)
| b18 `(t)
| b19 `(t)
| b20 `(t)
| b21 `(t)
| b22 `(t)
| b23 `(t)
| b24 `(t)
| b25 `(t)
| b26 `(t)
| b27 `(t)
| b28 `(t)
| b29 `(t)
| b30 `(t)
| b31 `(t)
| b32 `(t)
| b33 `(t)
| b34 `(t)
| b35 `(t)
| b36 `(t)
| b37 `(t)
| b38 `(t)
| b39 `(t)
| b40 `(t)
| b41 `(t)
| b42 `(t)
| b43 `(t)
| b44 `(t)
| b45 `(t)
| b46 `(t)
| b47 `(t)
| b48 `(t)
| b49 `(t)
| b50 `(t)
| b51 `(t)
| b52 `(t)
| b53 `(t)
| b54 `(t)
| b55 `(t)
| b56 `(t)
| b57 `(t)
| b58 `(t)
| b59 `(t)
| b60 `(t)
| b61 `(t)
| b62 `(t)
| b63 `(t)
| b64 `(t)
| b65 `(t)
| b66 `(t)
| b67 `(t)
| b68 `(t)
| b69 `(t)
| b70 `(t).

Record eqtype (A : Type) := {
  beq : A -> A -> bool;
  reflect_beq : forall x y, reflect (x = y) (beq x y)
}.

Fixpoint expand (l : list Type) t : Type :=
  match l with
  | [] => t
  | t1 :: l => t1 -> expand l t
  end.

Variant type (T : Type) {lt:T->T->Prop} (wf:well_founded lt):=
| extern : {A & eqtype A & T -> A} -> type T wf (* could be T -> option A *)
| self   : (forall t:T, option {t':T|lt t' t}) -> type T wf.
Arguments extern {_ _ _}.
Arguments self {_ _ _}.

Record constr_descr (T : Type) {lt:T->T->Prop} (wf:well_founded lt):= {
  types : list (type T wf);
  constructor : expand (map (fun t => match t with
                                      | extern t => projT1 (sigT_of_sigT2 t)
                                      | self _ => T
                                      end) types) T
}.

Fixpoint measure (x:t2) :=
  match x with
  | b2 _ x => S (measure x)
  | _ => 0
  end.
Require Import Wf_nat.
Definition wf := well_founded_ltof _ measure.

Definition B0 : constr_descr t2 wf := {|
  types := [];
  constructor := b0
|}.

Scheme Equality for t.
Lemma reflect_t_beq : forall x y, reflect (x = y) (t_beq x y).
Proof.
  intros. destruct (t_beq x y) eqn:heq; constructor.
  - apply internal_t_dec_bl. assumption.
  - intros contra. apply not_true_iff_false in heq. contradiction heq.
    apply internal_t_dec_lb. assumption.
Qed.

Definition t_eqtype : eqtype t := {|
  beq := t_beq;
  reflect_beq := reflect_t_beq
|}.

Definition B1 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _);
            extern (existT2 _ _ (t:Type) t_eqtype _);
            extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b1
|}.
- intros x. destruct x. 2:apply H. all: exact a0. (* default value *)
- intros x. destruct x. 2:apply H0. all: exact a0. (* default value *)
- intros x. destruct x. 2:apply H1. all: exact a0. (* default value *)
Defined.

Definition B2 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _); self _];
  constructor := b2
|}.
- intros x. destruct x. 3:assumption. all: exact a0. (* default value *)
- intros x. destruct x. 3:{ apply Some. exists x. unfold ltof. simpl. apply le_n. } all: exact None.
Defined.

Definition nat_eqtype := {|
  beq := Nat.eqb;
  reflect_beq := PeanoNat.Nat.eqb_spec
|}.

Definition B3 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (nat:Type) nat_eqtype _)];
  constructor := b3
|}.
intros x. destruct x. 4:assumption. all: exact 0. (* default value *)
Defined.

Definition bool_eqtype := {|
  beq := Bool.eqb;
  reflect_beq := Bool.eqb_spec
|}.

Definition B4 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (bool:Type) bool_eqtype _)];
  constructor := b4
|}.
intros x. destruct x. 5:assumption. all: exact false. (* default value *)
Defined.

Definition B5 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b5
|}.
intros x. destruct x. 6:assumption. all: exact a0. (* default value *)
Defined.

Definition B6 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b6
|}.
intros x. destruct x. 7:assumption. all: exact a0. (* default value *)
Defined.

Definition B7 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b7
|}.
intros x. destruct x. 8:assumption. all: exact a0. (* default value *)
Defined.

Definition B8 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b8
|}.
intros x. destruct x. 9:assumption. all: exact a0. (* default value *)
Defined.

Definition B9 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b9
|}.
intros x. destruct x. 10:assumption. all: exact a0. (* default value *)
Defined.

Definition B10 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b10
|}.
intros x. destruct x. 11:assumption. all: exact a0. (* default value *)
Defined.

Definition B11 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b11
|}.
intros x. destruct x. 12:assumption. all: exact a0. (* default value *)
Defined.

Definition B12 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b12
|}.
intros x. destruct x. 13:assumption. all: exact a0. (* default value *)
Defined.

Definition B13 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b13
|}.
intros x. destruct x. 14:assumption. all: exact a0. (* default value *)
Defined.

Definition B14 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b14
|}.
intros x. destruct x. 15:assumption. all: exact a0. (* default value *)
Defined.

Definition B15 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b15
|}.
intros x. destruct x. 16:assumption. all: exact a0. (* default value *)
Defined.

Definition B16 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b16
|}.
intros x. destruct x. 17:assumption. all: exact a0. (* default value *)
Defined.

Definition B17 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b17
|}.
intros x. destruct x. 18:assumption. all: exact a0. (* default value *)
Defined.

Definition B18 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b18
|}.
intros x. destruct x. 19:assumption. all: exact a0. (* default value *)
Defined.

Definition B19 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b19
|}.
intros x. destruct x. 20:assumption. all: exact a0. (* default value *)
Defined.

Definition B20 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b20
|}.
intros x. destruct x. 21:assumption. all: exact a0. (* default value *)
Defined.

Definition B21 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b21
|}.
intros x. destruct x. 22:assumption. all: exact a0. (* default value *)
Defined.

Definition B22 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b22
|}.
intros x. destruct x. 23:assumption. all: exact a0. (* default value *)
Defined.

Definition B23 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b23
|}.
intros x. destruct x. 24:assumption. all: exact a0. (* default value *)
Defined.

Definition B24 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b24
|}.
intros x. destruct x. 25:assumption. all: exact a0. (* default value *)
Defined.

Definition B25 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b25
|}.
intros x. destruct x. 26:assumption. all: exact a0. (* default value *)
Defined.

Definition B26 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b26
|}.
intros x. destruct x. 27:assumption. all: exact a0. (* default value *)
Defined.

Definition B27 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b27
|}.
intros x. destruct x. 28:assumption. all: exact a0. (* default value *)
Defined.

Definition B28 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b28
|}.
intros x. destruct x. 29:assumption. all: exact a0. (* default value *)
Defined.

Definition B29 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b29
|}.
intros x. destruct x. 30:assumption. all: exact a0. (* default value *)
Defined.

Definition B30 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b30
|}.
intros x. destruct x. 31:assumption. all: exact a0. (* default value *)
Defined.

Definition B31 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b31
|}.
intros x. destruct x. 32:assumption. all: exact a0. (* default value *)
Defined.

Definition B32 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b32
|}.
intros x. destruct x. 33:assumption. all: exact a0. (* default value *)
Defined.

Definition B33 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b33
|}.
intros x. destruct x. 34:assumption. all: exact a0. (* default value *)
Defined.

Definition B34 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b34
|}.
intros x. destruct x. 35:assumption. all: exact a0. (* default value *)
Defined.

Definition B35 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b35
|}.
intros x. destruct x. 36:assumption. all: exact a0. (* default value *)
Defined.

Definition B36 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b36
|}.
intros x. destruct x. 37:assumption. all: exact a0. (* default value *)
Defined.

Definition B37 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b37
|}.
intros x. destruct x. 38:assumption. all: exact a0. (* default value *)
Defined.

Definition B38 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b38
|}.
intros x. destruct x. 39:assumption. all: exact a0. (* default value *)
Defined.

Definition B39 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b39
|}.
intros x. destruct x. 40:assumption. all: exact a0. (* default value *)
Defined.

Definition B40 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b40
|}.
intros x. destruct x. 41:assumption. all: exact a0. (* default value *)
Defined.

Definition B41 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b41
|}.
intros x. destruct x. 42:assumption. all: exact a0. (* default value *)
Defined.

Definition B42 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b42
|}.
intros x. destruct x. 43:assumption. all: exact a0. (* default value *)
Defined.

Definition B43 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b43
|}.
intros x. destruct x. 44:assumption. all: exact a0. (* default value *)
Defined.

Definition B44 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b44
|}.
intros x. destruct x. 45:assumption. all: exact a0. (* default value *)
Defined.

Definition B45 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b45
|}.
intros x. destruct x. 46:assumption. all: exact a0. (* default value *)
Defined.

Definition B46 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b46
|}.
intros x. destruct x. 47:assumption. all: exact a0. (* default value *)
Defined.

Definition B47 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b47
|}.
intros x. destruct x. 48:assumption. all: exact a0. (* default value *)
Defined.

Definition B48 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b48
|}.
intros x. destruct x. 49:assumption. all: exact a0. (* default value *)
Defined.

Definition B49 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b49
|}.
intros x. destruct x. 50:assumption. all: exact a0. (* default value *)
Defined.

Definition B50 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b50
|}.
intros x. destruct x. 51:assumption. all: exact a0. (* default value *)
Defined.

Definition B51 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b51
|}.
intros x. destruct x. 52:assumption. all: exact a0. (* default value *)
Defined.

Definition B52 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b52
|}.
intros x. destruct x. 53:assumption. all: exact a0. (* default value *)
Defined.

Definition B53 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b53
|}.
intros x. destruct x. 54:assumption. all: exact a0. (* default value *)
Defined.

Definition B54 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b54
|}.
intros x. destruct x. 55:assumption. all: exact a0. (* default value *)
Defined.

Definition B55 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b55
|}.
intros x. destruct x. 56:assumption. all: exact a0. (* default value *)
Defined.

Definition B56 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b56
|}.
intros x. destruct x. 57:assumption. all: exact a0. (* default value *)
Defined.

Definition B57 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b57
|}.
intros x. destruct x. 58:assumption. all: exact a0. (* default value *)
Defined.

Definition B58 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b58
|}.
intros x. destruct x. 59:assumption. all: exact a0. (* default value *)
Defined.

Definition B59 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b59
|}.
intros x. destruct x. 60:assumption. all: exact a0. (* default value *)
Defined.

Definition B60 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b60
|}.
intros x. destruct x. 61:assumption. all: exact a0. (* default value *)
Defined.

Definition B61 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b61
|}.
intros x. destruct x. 62:assumption. all: exact a0. (* default value *)
Defined.

Definition B62 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b62
|}.
intros x. destruct x. 63:assumption. all: exact a0. (* default value *)
Defined.

Definition B63 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b63
|}.
intros x. destruct x. 64:assumption. all: exact a0. (* default value *)
Defined.

Definition B64 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b64
|}.
intros x. destruct x. 65:assumption. all: exact a0. (* default value *)
Defined.

Definition B65 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b65
|}.
intros x. destruct x. 66:assumption. all: exact a0. (* default value *)
Defined.

Definition B66 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b66
|}.
intros x. destruct x. 67:assumption. all: exact a0. (* default value *)
Defined.

Definition B67 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b67
|}.
intros x. destruct x. 68:assumption. all: exact a0. (* default value *)
Defined.

Definition B68 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b68
|}.
intros x. destruct x. 69:assumption. all: exact a0. (* default value *)
Defined.

Definition B69 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b69
|}.
intros x. destruct x. 70:assumption. all: exact a0. (* default value *)
Defined.

Definition B70 : constr_descr t2 wf. refine {|
  types := [extern (existT2 _ _ (t:Type) t_eqtype _)];
  constructor := b70
|}.
intros x. destruct x. 71:assumption. all: exact a0. (* default value *)
Defined.

Definition ls : list (constr_descr t2 wf) := [
B0;
B1;
B2;
B3;
B4;
B5;
B6;
B7;
B8;
B9;
B10;
B11;
B12;
B13;
B14;
B15;
B16;
B17;
B18;
B19;
B20;
B21;
B22;
B23;
B24;
B25;
B26;
B27;
B28;
B29;
B30;
B31;
B32;
B33;
B34;
B35;
B36;
B37;
B38;
B39;
B40;
B41;
B42;
B43;
B44;
B45;
B46;
B47;
B48;
B49;
B50;
B51;
B52;
B53;
B54;
B55;
B56;
B57;
B58;
B59;
B60;
B61;
B62;
B63;
B64;
B65;
B66;
B67;
B68;
B69;
B70
].

Section fin.
  Context (t: Type) (lt : t -> t -> Prop) (wf: well_founded lt)
          (ls : list (constr_descr t wf))
          (to_nat : t -> nat).
(*
  Fixpoint forallbi {A} (f : nat -> A -> bool) (l : list A) :=
    match l with
    | [] => true
    | a :: l => f 0 a && forallbi (fun n => f (S n)) l
    end.
*)
  Fixpoint beq_gen (x y : t) (H:Acc lt x) : bool.
  Proof.
    refine (
    let n_x := to_nat x in
    let n_y := to_nat y in
    if Nat.eqb n_x n_y then
      match nth_error ls n_x with
      | None => false (* unreachable *)
      | Some c => forallb (fun (c:type t wf) =>
        match c with
        | extern c =>
          let A := projT1 (sigT_of_sigT2 c) in
          let beq : A -> A -> bool := beq _ (projT2 (sigT_of_sigT2 c)) in
          let arg : t -> A := projT3 c in
          beq (arg x) (arg y)
        | self proj => (* recursive call *)
          match proj x, proj y with
          | Some projx, Some projy => beq_gen (proj1_sig projx) (proj1_sig projy) _
          | _, _ => false (* unreachable? *)
          end
        end
          ) c.(types _ _)
      end
    else false).
    apply H. apply (proj2_sig projx).
  Defined.

  Definition eval (l : list (type t wf))
    (c: expand (map (fun x => match x with
                                      | extern t => projT1 (sigT_of_sigT2 t)
                                      | self _ => t
                                      end) l) t) (x:t) : option t.
  Proof.
    revert l c x.
    fix eval 1. intros. destruct l. simpl in c. apply (Some c).
    simpl in c.
    destruct t0.
    + set (d := c (projT3 s x)).
      apply (eval l d x).
    + destruct (o x) as [x'|].
      * set (d := c (proj1_sig x')).
        apply (eval l d x).
      * apply None.
  Defined.

  Context (ls_has_all : forall e,
    match nth_error ls (to_nat e) with
    | Some c => eval (types _ _ c) (constructor _ _ c) e = Some e
    | None => False
    end).

Scheme df := Induction for Acc Sort Prop.
Lemma nth_error_beq x y : beq_gen x y (wf x) = true -> x = y.
Proof.
  generalize (wf x) y. induction a using df; intros y0.
  simpl.
  destruct (PeanoNat.Nat.eqb_spec (to_nat x) (to_nat y0)); [|discriminate].
  destruct nth_error as [c|] eqn:heq; [|discriminate].
  pose proof (ls_has_all x) as H1. rewrite heq in H1.
  pose proof (ls_has_all y0) as H2. rewrite <- e, heq in H2.
  pattern x at 8.
  change x with (match (Some x) with | Some y => y | None => x end) at 8.
  rewrite <- H1.
  pattern y0 at 6.
  change y0 with (match (Some y0) with | Some y => y | None => y0 end) at 6.
  rewrite <- H2. clear H1 H2 heq e.
  generalize (constructor t wf c) y0.
  induction (types t wf c).
  - simpl. reflexivity.
  - simpl. destruct a2.
    + destruct s as [A EQ proj]. simpl.
      intros ??. rewrite andb_true_iff. intros [heq HH].
      assert (proj x = proj y1) as Ha.
      { destruct (reflect_beq _ EQ (proj x) (proj y1)).
        assumption. discriminate.
      }
      apply IHl with (e:=e (proj x)) in HH.
      rewrite <- Ha. assumption.
    + intros ??. destruct (o x) as [x'|]; [|discriminate].
      destruct (o y1) as [y'|]; [|discriminate].
      rewrite andb_true_iff. intros [heq HH].
      assert ((proj1_sig x') = (proj1_sig y')) as Ha.
      { apply H in heq. assumption. }
      apply IHl with (e:=e (proj1_sig x')) in HH.
      rewrite <- Ha. assumption.
Qed.

Lemma reflect_of_fin : forall x y, reflect (x = y) (beq_gen x y (wf x)).
Proof.
  intros x y; remember (beq_gen x y (wf x)) as b eqn:Heqb; destruct b; symmetry in Heqb; constructor.
  { apply nth_error_beq. assumption. }
  { intro H. subst y.
    revert Heqb. generalize (wf x). induction a using df. simpl.
    rewrite PeanoNat.Nat.eqb_refl.
    specialize (ls_has_all x). destruct nth_error as [c|]; [|contradiction].
    revert ls_has_all. generalize (constructor t wf c).
    induction (types t wf c).
    - simpl. discriminate.
    - intros e ls_has_all. destruct a2.
      + destruct s as [A EQ proj]. simpl.
        rewrite andb_false_iff.
        intros [HH|HH].
        destruct (reflect_beq _ EQ (proj x) (proj x)). discriminate. contradiction.
        eapply IHl; eassumption.
      + simpl. simpl in ls_has_all. destruct (o x) as [projx|]; [|discriminate].
        rewrite andb_false_iff.
        intros [HH|HH].
        apply H in HH. contradiction.
        eapply IHl; eassumption.
  }
Qed.

End fin.

Definition to_nat x :=
  match x with
| b0 => 0
| b1 _ _ _ => 1
| b2 _ _ => 2
| b3 _ => 3
| b4 _ => 4
| b5 _ => 5
| b6 _ => 6
| b7 _ => 7
| b8 _ => 8
| b9 _ => 9
| b10 _ => 10
| b11 _ => 11
| b12 _ => 12
| b13 _ => 13
| b14 _ => 14
| b15 _ => 15
| b16 _ => 16
| b17 _ => 17
| b18 _ => 18
| b19 _ => 19
| b20 _ => 20
| b21 _ => 21
| b22 _ => 22
| b23 _ => 23
| b24 _ => 24
| b25 _ => 25
| b26 _ => 26
| b27 _ => 27
| b28 _ => 28
| b29 _ => 29
| b30 _ => 30
| b31 _ => 31
| b32 _ => 32
| b33 _ => 33
| b34 _ => 34
| b35 _ => 35
| b36 _ => 36
| b37 _ => 37
| b38 _ => 38
| b39 _ => 39
| b40 _ => 40
| b41 _ => 41
| b42 _ => 42
| b43 _ => 43
| b44 _ => 44
| b45 _ => 45
| b46 _ => 46
| b47 _ => 47
| b48 _ => 48
| b49 _ => 49
| b50 _ => 50
| b51 _ => 51
| b52 _ => 52
| b53 _ => 53
| b54 _ => 54
| b55 _ => 55
| b56 _ => 56
| b57 _ => 57
| b58 _ => 58
| b59 _ => 59
| b60 _ => 60
| b61 _ => 61
| b62 _ => 62
| b63 _ => 63
| b64 _ => 64
| b65 _ => 65
| b66 _ => 66
| b67 _ => 67
| b68 _ => 68
| b69 _ => 69
| b70 _ => 70
  end.

Lemma ls_has_all : forall e,
    match nth_error ls (to_nat e) with
    | Some c => eval t2 _ _ (types _ _ c) (constructor _ _ c) e = Some e
    | None => False
    end.
Proof. destruct e; reflexivity. Qed.

Definition t2_beq x y := beq_gen _ _ _ ls to_nat x y (wf x).

Lemma reflect_t2_beq : forall x y, reflect (x = y) (t2_beq x y).
Proof. apply reflect_of_fin. apply ls_has_all. Qed.

Eval compute in t2_beq (b2 a0 (b3 5)) (b2 a0 (b3 500000)).