From Undecidability.Shared.Libs.PSL Require Prelim.
From Coq.Vectors Require Import Vector Fin.
From Undecidability.Shared.Libs.PSL Require Import FiniteTypes.FinTypes.

Class inhabitedC (X : Type) :=
    {
      default : X;
    }.

#[global]
Instance inhabited_unit : inhabitedC unit.
Proof. do 2 constructor. Defined.

#[global]
Instance inhabited_True : inhabitedC True.
Proof. do 2 constructor. Defined.

#[global]
Instance inhabited_inl (A B : Type) (inh_a : inhabitedC A) : inhabitedC (A + B).
Proof. constructor. left. apply default. Defined.

#[global]
Instance inhabited_inr (A B : Type) (inh_B : inhabitedC B) : inhabitedC (A + B).
Proof. constructor. right. apply default. Defined.

#[global]
Instance inhabited_option (A : Type) : inhabitedC (option A).
Proof. constructor. right. Defined.

#[global]
Instance inhabited_bool : inhabitedC bool.
Proof. do 2 constructor. Defined.

#[global]
Instance inhabited_list (A : Type) : inhabitedC (list A).
Proof. do 2 constructor. Defined.

#[global]
Instance inhabited_vector (A : Type) (n : nat) (inh_A : inhabitedC A) : inhabitedC (Vector.t A n).
Proof. constructor. eapply VectorDef.const. apply default. Defined.

#[global]
Instance inhabited_fin (n : nat) : inhabitedC (Fin.t (S n)).
Proof. repeat constructor. Defined.

#[global]
Instance inhabited_nat : inhabitedC nat.
Proof. do 2 constructor. Defined.

#[global]
Instance inhabited_prod (A B : Type) : inhabitedC A -> inhabitedC B -> inhabitedC (A*B).
Proof. intros ia ib. do 2 constructor; apply default. Defined.

#[global]
Instance inhabited_arrow (A B : Type) : inhabitedC B -> inhabitedC (A -> B).
Proof. intros. constructor. intros _. apply default. Defined.

#[global]
Instance inhabited_arrow_empty (B : Type) : inhabitedC (Empty_set -> B).
Proof. intros. constructor. apply Empty_set_rect. Defined.

#[global]
Instance inhabited_arrow_sum (A B C : Type) : inhabitedC (A->C) -> inhabitedC (B->C) -> inhabitedC (A+B->C).
Proof. intros iac ibc. constructor. intros [?|?]. now apply iac. now apply ibc. Defined.

#[global]
Instance inhabited_arrow_prod (A B C : Type) : inhabitedC (A->B) -> inhabitedC (A->C) -> inhabitedC (A->B*C).
Proof. intros iab iac. constructor. intros a. constructor. now apply iab. now apply iac. Defined.

#[export] Hint Extern 10 => match goal with
                | [ H : ?X |- inhabitedC ?X ] => now econstructor
                end : typeclass_instances.