text:
(* Default settings (from HsToCoq.Coq.Preamble) *)

Generalizable All Variables.

Unset Implicit Arguments.
Set Maximal Implicit Insertion.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Require Coq.Program.Tactics.
Require Coq.Program.Wf.

(* Preamble *)

(* A hack to make a few kind-polymorpic definitions go through *)
Class unit_class.
Instance unit_class_instance : unit_class := {}.
Implicit Type inst_k: unit_class.

(* Converted imports: *)

Require GHC.Base.
Require GHC.Err.
Require GHC.Num.
Require GHC.Prim.
Require GHC.Real.
Require HsToCoq.Err.
Require HsToCoq.Unpeel.
Import GHC.Base.Notations.
Import GHC.Num.Notations.

(* Converted type declarations: *)

Inductive Sum a : Type := | Mk_Sum (getSum : a) : Sum a.

Inductive Product a : Type := | Mk_Product (getProduct : a) : Product a.

Inductive Endo a : Type := | Mk_Endo (appEndo : a -> a) : Endo a.

Inductive Dual a : Type := | Mk_Dual (getDual : a) : Dual a.

Inductive Any : Type := | Mk_Any (getAny : bool) : Any.

Inductive Alt {k : Type} (f : k -> Type) (a : k) : Type :=
  | Mk_Alt (getAlt : f a) : Alt f a.

Inductive All : Type := | Mk_All (getAll : bool) : All.

Arguments Mk_Sum {_} _.

Arguments Mk_Product {_} _.

Arguments Mk_Endo {_} _.

Arguments Mk_Dual {_} _.

Arguments Mk_Alt {_} {_} {_} _.

Instance Default__Any : HsToCoq.Err.Default Any :=
  HsToCoq.Err.Build_Default _ (Mk_Any HsToCoq.Err.default).

Instance Default__All : HsToCoq.Err.Default All :=
  HsToCoq.Err.Build_Default _ (Mk_All HsToCoq.Err.default).

Definition getSum {a} (arg_0__ : Sum a) :=
  let 'Mk_Sum getSum := arg_0__ in
  getSum.

Definition getProduct {a} (arg_0__ : Product a) :=
  let 'Mk_Product getProduct := arg_0__ in
  getProduct.

Definition appEndo {a} (arg_0__ : Endo a) :=
  let 'Mk_Endo appEndo := arg_0__ in
  appEndo.

Definition getDual {a} (arg_0__ : Dual a) :=
  let 'Mk_Dual getDual := arg_0__ in
  getDual.

Definition getAny (arg_0__ : Any) :=
  let 'Mk_Any getAny := arg_0__ in
  getAny.

Definition getAlt {k : Type} {f : k -> Type} {a : k} (arg_0__ : Alt f a) :=
  let 'Mk_Alt getAlt := arg_0__ in
  getAlt.

Definition getAll (arg_0__ : All) :=
  let 'Mk_All getAll := arg_0__ in
  getAll.

(* Midamble *)

Instance Unpeel_Alt (k : Type) (f : k -> Type) (a : k) : HsToCoq.Unpeel.Unpeel (Alt f a) (f a) :=
    HsToCoq.Unpeel.Build_Unpeel _ _ getAlt Mk_Alt.

(* Converted value declarations: *)

Instance Unpeel_Dual a : HsToCoq.Unpeel.Unpeel (Dual a) a :=
  HsToCoq.Unpeel.Build_Unpeel _ _ getDual Mk_Dual.

Local Definition Eq___Dual_op_zeze__ {inst_a : Type} `{GHC.Base.Eq_ inst_a}
   : Dual inst_a -> Dual inst_a -> bool :=
  GHC.Prim.coerce _GHC.Base.==_.

Local Definition Eq___Dual_op_zsze__ {inst_a : Type} `{GHC.Base.Eq_ inst_a}
   : Dual inst_a -> Dual inst_a -> bool :=
  GHC.Prim.coerce _GHC.Base./=_.

Program Instance Eq___Dual {a : Type} `{GHC.Base.Eq_ a}
   : GHC.Base.Eq_ (Dual a) :=
  fun _ k__ =>
    k__ {| GHC.Base.op_zeze____ := Eq___Dual_op_zeze__ ;
           GHC.Base.op_zsze____ := Eq___Dual_op_zsze__ |}.

Local Definition Ord__Dual_op_zl__ {inst_a : Type} `{GHC.Base.Ord inst_a}
   : Dual inst_a -> Dual inst_a -> bool :=
  GHC.Prim.coerce _GHC.Base.<_.

Local Definition Ord__Dual_op_zlze__ {inst_a : Type} `{GHC.Base.Ord inst_a}
   : Dual inst_a -> Dual inst_a -> bool :=
  GHC.Prim.coerce _GHC.Base.<=_.

Local Definition Ord__Dual_op_zg__ {inst_a : Type} `{GHC.Base.Ord inst_a}
   : Dual inst_a -> Dual inst_a -> bool :=
  GHC.Prim.coerce _GHC.Base.>_.

Local Definition Ord__Dual_op_zgze__ {inst_a : Type} `{GHC.Base.Ord inst_a}
   : Dual inst_a -> Dual inst_a -> bool :=
  GHC.Prim.coerce _GHC.Base.>=_.

Local Definition Ord__Dual_compare {inst_a : Type} `{GHC.Base.Ord inst_a}
   : Dual inst_a -> Dual inst_a -> comparison :=
  GHC.Prim.coerce GHC.Base.compare.

Local Definition Ord__Dual_max {inst_a : Type} `{GHC.Base.Ord inst_a}
   : Dual inst_a -> Dual inst_a -> Dual inst_a :=
  GHC.Prim.coerce GHC.Base.max.

Local Definition Ord__Dual_min {inst_a : Type} `{GHC.Base.Ord inst_a}
   : Dual inst_a -> Dual inst_a -> Dual inst_a :=
  GHC.Prim.coerce GHC.Base.min.

Program Instance Ord__Dual {a : Type} `{GHC.Base.Ord a}
   : GHC.Base.Ord (Dual a) :=
  fun _ k__ =>
    k__ {| GHC.Base.op_zl____ := Ord__Dual_op_zl__ ;
           GHC.Base.op_zlze____ := Ord__Dual_op_zlze__ ;
           GHC.Base.op_zg____ := Ord__Dual_op_zg__ ;
           GHC.Base.op_zgze____ := Ord__Dual_op_zgze__ ;
           GHC.Base.compare__ := Ord__Dual_compare ;
           GHC.Base.max__ := Ord__Dual_max ;
           GHC.Base.min__ := Ord__Dual_min |}.

(* Skipping all instances of class `GHC.Read.Read', including
   `Data.SemigroupInternal.Read__Dual' *)

(* Skipping all instances of class `GHC.Show.Show', including
   `Data.SemigroupInternal.Show__Dual' *)

(* Skipping all instances of class `GHC.Enum.Bounded', including
   `Data.SemigroupInternal.Bounded__Dual' *)

(* Skipping all instances of class `GHC.Generics.Generic', including
   `Data.SemigroupInternal.Generic__Dual' *)

(* Skipping all instances of class `GHC.Generics.Generic1', including
   `Data.SemigroupInternal.Generic1__TYPE__Dual__LiftedRep' *)

(* Skipping all instances of class `GHC.Generics.Generic', including
   `Data.SemigroupInternal.Generic__Endo' *)

Instance Unpeel_All : HsToCoq.Unpeel.Unpeel All bool :=
  HsToCoq.Unpeel.Build_Unpeel _ _ getAll Mk_All.

Local Definition Eq___All_op_zeze__ : All -> All -> bool :=
  GHC.Prim.coerce _GHC.Base.==_.

Local Definition Eq___All_op_zsze__ : All -> All -> bool :=
  GHC.Prim.coerce _GHC.Base./=_.

Program Instance Eq___All : GHC.Base.Eq_ All :=
  fun _ k__ =>
    k__ {| GHC.Base.op_zeze____ := Eq___All_op_zeze__ ;
           GHC.Base.op_zsze____ := Eq___All_op_zsze__ |}.

Local Definition Ord__All_op_zl__ : All -> All -> bool :=
  GHC.Prim.coerce _GHC.Base.<_.

Local Definition Ord__All_op_zlze__ : All -> All -> bool :=
  GHC.Prim.coerce _GHC.Base.<=_.

Local Definition Ord__All_op_zg__ : All -> All -> bool :=
  GHC.Prim.coerce _GHC.Base.>_.

Local Definition Ord__All_op_zgze__ : All -> All -> bool :=
  GHC.Prim.coerce _GHC.Base.>=_.

Local Definition Ord__All_compare : All -> All -> comparison :=
  GHC.Prim.coerce GHC.Base.compare.

Local Definition Ord__All_max : All -> All -> All :=
  GHC.Prim.coerce GHC.Base.max.

Local Definition Ord__All_min : All -> All -> All :=
  GHC.Prim.coerce GHC.Base.min.

Program Instance Ord__All : GHC.Base.Ord All :=
  fun _ k__ =>
    k__ {| GHC.Base.op_zl____ := Ord__All_op_zl__ ;
           GHC.Base.op_zlze____ := Ord__All_op_zlze__ ;
           GHC.Base.op_zg____ := Ord__All_op_zg__ ;
           GHC.Base.op_zgze____ := Ord__All_op_zgze__ ;
           GHC.Base.compare__ := Ord__All_compare ;
           GHC.Base.max__ := Ord__All_max ;
           GHC.Base.min__ := Ord__All_min |}.

(* Skipping all instances of class `GHC.Read.Read', including
   `Data.SemigroupInternal.Read__All' *)

(* Skipping all instances of class `GHC.Show.Show', including
   `Data.SemigroupInternal.Show__All' *)

(* Skipping all instances of class `GHC.Enum.Bounded', including
   `Data.SemigroupInternal.Bounded__All' *)

(* Skipping all instances of class `GHC.Generics.Generic', including
   `Data.SemigroupInternal.Generic__All' *)

Instance Unpeel_Any : HsToCoq.Unpeel.Unpeel Any bool :=
  HsToCoq.Unpeel.Build_Unpeel _ _ getAny Mk_Any.

Local Definition Eq___Any_op_zeze__ : Any -> Any -> bool :=
  GHC.Prim.coerce _GHC.Base.==_.

Local Definition Eq___Any_op_zsze__ : Any -> Any -> bool :=
  GHC.Prim.coerce _GHC.Base./=_.

Program Instance Eq___Any : GHC.Base.Eq_ Any :=
  fun _ k__ =>
    k__ {| GHC.Base.op_zeze____ := Eq___Any_op_zeze__ ;
           GHC.Base.op_zsze____ := Eq___Any_op_zsze__ |}.

Local Definition Ord__Any_op_zl__ : Any -> Any -> bool :=
  GHC.Prim.coerce _GHC.Base.<_.

Local Definition Ord__Any_op_zlze__ : Any -> Any -> bool :=
  GHC.Prim.coerce _GHC.Base.<=_.

Local Definition Ord__Any_op_zg__ : Any -> Any -> bool :=
  GHC.Prim.coerce _GHC.Base.>_.

Local Definition Ord__Any_op_zgze__ : Any -> Any -> bool :=
  GHC.Prim.coerce _GHC.Base.>=_.

Local Definition Ord__Any_compare : Any -> Any -> comparison :=
  GHC.Prim.coerce GHC.Base.compare.

Local Definition Ord__Any_max : Any -> Any -> Any :=
  GHC.Prim.coerce GHC.Base.max.

Local Definition Ord__Any_min : Any -> Any -> Any :=
  GHC.Prim.coerce GHC.Base.min.

Program Instance Ord__Any : GHC.Base.Ord Any :=
  fun _ k__ =>
    k__ {| GHC.Base.op_zl____ := Ord__Any_op_zl__ ;
           GHC.Base.op_zlze____ := Ord__Any_op_zlze__ ;
           GHC.Base.op_zg____ := Ord__Any_op_zg__ ;
           GHC.Base.op_zgze____ := Ord__Any_op_zgze__ ;
           GHC.Base.compare__ := Ord__Any_compare ;
           GHC.Base.max__ := Ord__Any_max ;
           GHC.Base.min__ := Ord__Any_min |}.

(* Skipping all instances of class `GHC.Read.Read', including
   `Data.SemigroupInternal.Read__Any' *)

(* Skipping all instances of class `GHC.Show.Show', including
   `Data.SemigroupInternal.Show__Any' *)

(* Skipping all instances of class `GHC.Enum.Bounded', including
   `Data.SemigroupInternal.Bounded__Any' *)

(* Skipping all instances of class `GHC.Generics.Generic', including
   `Data.SemigroupInternal.Generic__Any' *)

Instance Unpeel_Sum a : HsToCoq.Unpeel.Unpeel (Sum a) a :=
  HsToCoq.Unpeel.Build_Unpeel _ _ getSum Mk_Sum.

Local Definition Eq___Sum_op_zeze__ {inst_a : Type} `{GHC.Base.Eq_ inst_a}
   : Sum inst_a -> Sum inst_a -> bool :=
  GHC.Prim.coerce _GHC.Base.==_.

Local Definition Eq___Sum_op_zsze__ {inst_a : Type} `{GHC.Base.Eq_ inst_a}
   : Sum inst_a -> Sum inst_a -> bool :=
  GHC.Prim.coerce _GHC.Base./=_.

Program Instance Eq___Sum {a : Type} `{GHC.Base.Eq_ a} : GHC.Base.Eq_ (Sum a) :=
  fun _ k__ =>
    k__ {| GHC.Base.op_zeze____ := Eq___Sum_op_zeze__ ;
           GHC.Base.op_zsze____ := Eq___Sum_op_zsze__ |}.

Local Definition Ord__Sum_op_zl__ {inst_a : Type} `{GHC.Base.Ord inst_a}
   : Sum inst_a -> Sum inst_a -> bool :=
  GHC.Prim.coerce _GHC.Base.<_.

Local Definition Ord__Sum_op_zlze__ {inst_a : Type} `{GHC.Base.Ord inst_a}
   : Sum inst_a -> Sum inst_a -> bool :=
  GHC.Prim.coerce _GHC.Base.<=_.

Local Definition Ord__Sum_op_zg__ {inst_a : Type} `{GHC.Base.Ord inst_a}
   : Sum inst_a -> Sum inst_a -> bool :=
  GHC.Prim.coerce _GHC.Base.>_.

Local Definition Ord__Sum_op_zgze__ {inst_a : Type} `{GHC.Base.Ord inst_a}
   : Sum inst_a -> Sum inst_a -> bool :=
  GHC.Prim.coerce _GHC.Base.>=_.

Local Definition Ord__Sum_compare {inst_a : Type} `{GHC.Base.Ord inst_a}
   : Sum inst_a -> Sum inst_a -> comparison :=
  GHC.Prim.coerce GHC.Base.compare.

Local Definition Ord__Sum_max {inst_a : Type} `{GHC.Base.Ord inst_a}
   : Sum inst_a -> Sum inst_a -> Sum inst_a :=
  GHC.Prim.coerce GHC.Base.max.

Local Definition Ord__Sum_min {inst_a : Type} `{GHC.Base.Ord inst_a}
   : Sum inst_a -> Sum inst_a -> Sum inst_a :=
  GHC.Prim.coerce GHC.Base.min.

Program Instance Ord__Sum {a : Type} `{GHC.Base.Ord a} : GHC.Base.Ord (Sum a) :=
  fun _ k__ =>
    k__ {| GHC.Base.op_zl____ := Ord__Sum_op_zl__ ;
           GHC.Base.op_zlze____ := Ord__Sum_op_zlze__ ;
           GHC.Base.op_zg____ := Ord__Sum_op_zg__ ;
           GHC.Base.op_zgze____ := Ord__Sum_op_zgze__ ;
           GHC.Base.compare__ := Ord__Sum_compare ;
           GHC.Base.max__ := Ord__Sum_max ;
           GHC.Base.min__ := Ord__Sum_min |}.

(* Skipping all instances of class `GHC.Read.Read', including
   `Data.SemigroupInternal.Read__Sum' *)

(* Skipping all instances of class `GHC.Show.Show', including
   `Data.SemigroupInternal.Show__Sum' *)

(* Skipping all instances of class `GHC.Enum.Bounded', including
   `Data.SemigroupInternal.Bounded__Sum' *)

(* Skipping all instances of class `GHC.Generics.Generic', including
   `Data.SemigroupInternal.Generic__Sum' *)

(* Skipping all instances of class `GHC.Generics.Generic1', including
   `Data.SemigroupInternal.Generic1__TYPE__Sum__LiftedRep' *)

(* Skipping all instances of class `GHC.Num.Num', including
   `Data.SemigroupInternal.Num__Sum' *)

Instance Unpeel_Product a : HsToCoq.Unpeel.Unpeel (Product a) a :=
  HsToCoq.Unpeel.Build_Unpeel _ _ getProduct Mk_Product.

Local Definition Eq___Product_op_zeze__ {inst_a : Type} `{GHC.Base.Eq_ inst_a}
   : Product inst_a -> Product inst_a -> bool :=
  GHC.Prim.coerce _GHC.Base.==_.

Local Definition Eq___Product_op_zsze__ {inst_a : Type} `{GHC.Base.Eq_ inst_a}
   : Product inst_a -> Product inst_a -> bool :=
  GHC.Prim.coerce _GHC.Base./=_.

Program Instance Eq___Product {a : Type} `{GHC.Base.Eq_ a}
   : GHC.Base.Eq_ (Product a) :=
  fun _ k__ =>
    k__ {| GHC.Base.op_zeze____ := Eq___Product_op_zeze__ ;
           GHC.Base.op_zsze____ := Eq___Product_op_zsze__ |}.

Local Definition Ord__Product_op_zl__ {inst_a : Type} `{GHC.Base.Ord inst_a}
   : Product inst_a -> Product inst_a -> bool :=
  GHC.Prim.coerce _GHC.Base.<_.

Local Definition Ord__Product_op_zlze__ {inst_a : Type} `{GHC.Base.Ord inst_a}
   : Product inst_a -> Product inst_a -> bool :=
  GHC.Prim.coerce _GHC.Base.<=_.

Local Definition Ord__Product_op_zg__ {inst_a : Type} `{GHC.Base.Ord inst_a}
   : Product inst_a -> Product inst_a -> bool :=
  GHC.Prim.coerce _GHC.Base.>_.

Local Definition Ord__Product_op_zgze__ {inst_a : Type} `{GHC.Base.Ord inst_a}
   : Product inst_a -> Product inst_a -> bool :=
  GHC.Prim.coerce _GHC.Base.>=_.

Local Definition Ord__Product_compare {inst_a : Type} `{GHC.Base.Ord inst_a}
   : Product inst_a -> Product inst_a -> comparison :=
  GHC.Prim.coerce GHC.Base.compare.

Local Definition Ord__Product_max {inst_a : Type} `{GHC.Base.Ord inst_a}
   : Product inst_a -> Product inst_a -> Product inst_a :=
  GHC.Prim.coerce GHC.Base.max.

Local Definition Ord__Product_min {inst_a : Type} `{GHC.Base.Ord inst_a}
   : Product inst_a -> Product inst_a -> Product inst_a :=
  GHC.Prim.coerce GHC.Base.min.

Program Instance Ord__Product {a : Type} `{GHC.Base.Ord a}
   : GHC.Base.Ord (Product a) :=
  fun _ k__ =>
    k__ {| GHC.Base.op_zl____ := Ord__Product_op_zl__ ;
           GHC.Base.op_zlze____ := Ord__Product_op_zlze__ ;
           GHC.Base.op_zg____ := Ord__Product_op_zg__ ;
           GHC.Base.op_zgze____ := Ord__Product_op_zgze__ ;
           GHC.Base.compare__ := Ord__Product_compare ;
           GHC.Base.max__ := Ord__Product_max ;
           GHC.Base.min__ := Ord__Product_min |}.

(* Skipping all instances of class `GHC.Read.Read', including
   `Data.SemigroupInternal.Read__Product' *)

(* Skipping all instances of class `GHC.Show.Show', including
   `Data.SemigroupInternal.Show__Product' *)

(* Skipping all instances of class `GHC.Enum.Bounded', including
   `Data.SemigroupInternal.Bounded__Product' *)

(* Skipping all instances of class `GHC.Generics.Generic', including
   `Data.SemigroupInternal.Generic__Product' *)

(* Skipping all instances of class `GHC.Generics.Generic1', including
   `Data.SemigroupInternal.Generic1__TYPE__Product__LiftedRep' *)

(* Skipping all instances of class `GHC.Num.Num', including
   `Data.SemigroupInternal.Num__Product' *)

(* Skipping all instances of class `GHC.Generics.Generic', including
   `Data.SemigroupInternal.Generic__Alt' *)

(* Skipping all instances of class `GHC.Generics.Generic1', including
   `Data.SemigroupInternal.Generic1__Alt__5' *)

(* Skipping all instances of class `GHC.Read.Read', including
   `Data.SemigroupInternal.Read__Alt' *)

(* Skipping all instances of class `GHC.Show.Show', including
   `Data.SemigroupInternal.Show__Alt' *)

Local Definition Eq___Alt_op_zeze__ {inst_k : Type} {inst_f : inst_k -> Type}
  {inst_a : inst_k} `{GHC.Base.Eq_ (inst_f inst_a)}
   : Alt inst_f inst_a -> Alt inst_f inst_a -> bool :=
  GHC.Prim.coerce _GHC.Base.==_.

Local Definition Eq___Alt_op_zsze__ {inst_k : Type} {inst_f : inst_k -> Type}
  {inst_a : inst_k} `{GHC.Base.Eq_ (inst_f inst_a)}
   : Alt inst_f inst_a -> Alt inst_f inst_a -> bool :=
  GHC.Prim.coerce _GHC.Base./=_.

Program Instance Eq___Alt {k : Type} {f : k -> Type} {a : k} `{GHC.Base.Eq_ (f
                                                                             a)}
   : GHC.Base.Eq_ (Alt f a) :=
  fun _ k__ =>
    k__ {| GHC.Base.op_zeze____ := Eq___Alt_op_zeze__ ;
           GHC.Base.op_zsze____ := Eq___Alt_op_zsze__ |}.

Local Definition Ord__Alt_op_zl__ {inst_k : Type} {inst_f : inst_k -> Type}
  {inst_a : inst_k} `{GHC.Base.Ord (inst_f inst_a)}
   : Alt inst_f inst_a -> Alt inst_f inst_a -> bool :=
  GHC.Prim.coerce _GHC.Base.<_.

Local Definition Ord__Alt_op_zlze__ {inst_k : Type} {inst_f : inst_k -> Type}
  {inst_a : inst_k} `{GHC.Base.Ord (inst_f inst_a)}
   : Alt inst_f inst_a -> Alt inst_f inst_a -> bool :=
  GHC.Prim.coerce _GHC.Base.<=_.

Local Definition Ord__Alt_op_zg__ {inst_k : Type} {inst_f : inst_k -> Type}
  {inst_a : inst_k} `{GHC.Base.Ord (inst_f inst_a)}
   : Alt inst_f inst_a -> Alt inst_f inst_a -> bool :=
  GHC.Prim.coerce _GHC.Base.>_.

Local Definition Ord__Alt_op_zgze__ {inst_k : Type} {inst_f : inst_k -> Type}
  {inst_a : inst_k} `{GHC.Base.Ord (inst_f inst_a)}
   : Alt inst_f inst_a -> Alt inst_f inst_a -> bool :=
  GHC.Prim.coerce _GHC.Base.>=_.

Local Definition Ord__Alt_compare {inst_k : Type} {inst_f : inst_k -> Type}
  {inst_a : inst_k} `{GHC.Base.Ord (inst_f inst_a)}
   : Alt inst_f inst_a -> Alt inst_f inst_a -> comparison :=
  GHC.Prim.coerce GHC.Base.compare.

Local Definition Ord__Alt_max {inst_k : Type} {inst_f : inst_k -> Type} {inst_a
   : inst_k} `{GHC.Base.Ord (inst_f inst_a)}
   : Alt inst_f inst_a -> Alt inst_f inst_a -> Alt inst_f inst_a :=
  GHC.Prim.coerce GHC.Base.max.

Local Definition Ord__Alt_min {inst_k : Type} {inst_f : inst_k -> Type} {inst_a
   : inst_k} `{GHC.Base.Ord (inst_f inst_a)}
   : Alt inst_f inst_a -> Alt inst_f inst_a -> Alt inst_f inst_a :=
  GHC.Prim.coerce GHC.Base.min.

Program Instance Ord__Alt {k : Type} {f : k -> Type} {a : k} `{GHC.Base.Ord (f
                                                                             a)}
   : GHC.Base.Ord (Alt f a) :=
  fun _ k__ =>
    k__ {| GHC.Base.op_zl____ := Ord__Alt_op_zl__ ;
           GHC.Base.op_zlze____ := Ord__Alt_op_zlze__ ;
           GHC.Base.op_zg____ := Ord__Alt_op_zg__ ;
           GHC.Base.op_zgze____ := Ord__Alt_op_zgze__ ;
           GHC.Base.compare__ := Ord__Alt_compare ;
           GHC.Base.max__ := Ord__Alt_max ;
           GHC.Base.min__ := Ord__Alt_min |}.

(* Skipping all instances of class `GHC.Num.Num', including
   `Data.SemigroupInternal.Num__Alt' *)

(* Skipping all instances of class `GHC.Enum.Enum', including
   `Data.SemigroupInternal.Enum__Alt' *)

Local Definition Monad__Alt_op_zgzg__ {inst_f : Type -> Type} `{GHC.Base.Monad
  inst_f}
   : forall {a : Type},
     forall {b : Type}, Alt inst_f a -> Alt inst_f b -> Alt inst_f b :=
  fun {a : Type} {b : Type} => GHC.Prim.coerce _GHC.Base.>>_.

Local Definition Monad__Alt_op_zgzgze__ {inst_f : Type -> Type} `{GHC.Base.Monad
  inst_f}
   : forall {a : Type},
     forall {b : Type}, Alt inst_f a -> (a -> Alt inst_f b) -> Alt inst_f b :=
  fun {a : Type} {b : Type} => GHC.Prim.coerce _GHC.Base.>>=_.

Local Definition Monad__Alt_return_ {inst_f : Type -> Type} `{GHC.Base.Monad
  inst_f}
   : forall {a : Type}, a -> Alt inst_f a :=
  fun {a : Type} => GHC.Prim.coerce GHC.Base.return_.

Local Definition Applicative__Alt_liftA2 {inst_f : Type -> Type}
  `{GHC.Base.Applicative inst_f}
   : forall {a : Type},
     forall {b : Type},
     forall {c : Type},
     (a -> b -> c) -> Alt inst_f a -> Alt inst_f b -> Alt inst_f c :=
  fun {a : Type} {b : Type} {c : Type} => GHC.Prim.coerce GHC.Base.liftA2.

Local Definition Applicative__Alt_op_zlztzg__ {inst_f : Type -> Type}
  `{GHC.Base.Applicative inst_f}
   : forall {a : Type},
     forall {b : Type}, Alt inst_f (a -> b) -> Alt inst_f a -> Alt inst_f b :=
  fun {a : Type} {b : Type} => GHC.Prim.coerce _GHC.Base.<*>_.

Local Definition Applicative__Alt_op_ztzg__ {inst_f : Type -> Type}
  `{GHC.Base.Applicative inst_f}
   : forall {a : Type},
     forall {b : Type}, Alt inst_f a -> Alt inst_f b -> Alt inst_f b :=
  fun {a : Type} {b : Type} => GHC.Prim.coerce _GHC.Base.*>_.

Local Definition Applicative__Alt_pure {inst_f : Type -> Type}
  `{GHC.Base.Applicative inst_f}
   : forall {a : Type}, a -> Alt inst_f a :=
  fun {a : Type} => GHC.Prim.coerce GHC.Base.pure.

Local Definition Functor__Alt_fmap {inst_f : Type -> Type} `{GHC.Base.Functor
  inst_f}
   : forall {a : Type},
     forall {b : Type}, (a -> b) -> Alt inst_f a -> Alt inst_f b :=
  fun {a : Type} {b : Type} => GHC.Prim.coerce GHC.Base.fmap.

Local Definition Functor__Alt_op_zlzd__ {inst_f : Type -> Type}
  `{GHC.Base.Functor inst_f}
   : forall {a : Type}, forall {b : Type}, a -> Alt inst_f b -> Alt inst_f a :=
  fun {a : Type} {b : Type} => GHC.Prim.coerce _GHC.Base.<$_.

Program Instance Functor__Alt {f : Type -> Type} `{GHC.Base.Functor f}
   : GHC.Base.Functor (Alt f) :=
  fun _ k__ =>
    k__ {| GHC.Base.fmap__ := fun {a : Type} {b : Type} => Functor__Alt_fmap ;
           GHC.Base.op_zlzd____ := fun {a : Type} {b : Type} => Functor__Alt_op_zlzd__ |}.

Program Instance Applicative__Alt {f : Type -> Type} `{GHC.Base.Applicative f}
   : GHC.Base.Applicative (Alt f) :=
  fun _ k__ =>
    k__ {| GHC.Base.liftA2__ := fun {a : Type} {b : Type} {c : Type} =>
             Applicative__Alt_liftA2 ;
           GHC.Base.op_zlztzg____ := fun {a : Type} {b : Type} =>
             Applicative__Alt_op_zlztzg__ ;
           GHC.Base.op_ztzg____ := fun {a : Type} {b : Type} =>
             Applicative__Alt_op_ztzg__ ;
           GHC.Base.pure__ := fun {a : Type} => Applicative__Alt_pure |}.

Program Instance Monad__Alt {f : Type -> Type} `{GHC.Base.Monad f}
   : GHC.Base.Monad (Alt f) :=
  fun _ k__ =>
    k__ {| GHC.Base.op_zgzg____ := fun {a : Type} {b : Type} =>
             Monad__Alt_op_zgzg__ ;
           GHC.Base.op_zgzgze____ := fun {a : Type} {b : Type} => Monad__Alt_op_zgzgze__ ;
           GHC.Base.return___ := fun {a : Type} => Monad__Alt_return_ |}.

(* Skipping all instances of class `GHC.Base.MonadPlus', including
   `Data.SemigroupInternal.MonadPlus__Alt' *)

(* Skipping all instances of class `GHC.Base.Alternative', including
   `Data.SemigroupInternal.Alternative__Alt' *)

Local Definition Semigroup__Dual_op_zlzlzgzg__ {inst_a : Type}
  `{GHC.Base.Semigroup inst_a}
   : Dual inst_a -> Dual inst_a -> Dual inst_a :=
  fun arg_0__ arg_1__ =>
    match arg_0__, arg_1__ with
    | Mk_Dual a, Mk_Dual b => Mk_Dual (b GHC.Base.<<>> a)
    end.

Program Instance Semigroup__Dual {a : Type} `{GHC.Base.Semigroup a}
   : GHC.Base.Semigroup (Dual a) :=
  fun _ k__ =>
    k__ {| GHC.Base.op_zlzlzgzg____ := Semigroup__Dual_op_zlzlzgzg__ |}.

Local Definition Monoid__Dual_mappend {inst_a : Type} `{GHC.Base.Monoid inst_a}
   : Dual inst_a -> Dual inst_a -> Dual inst_a :=
  _GHC.Base.<<>>_.

Local Definition Monoid__Dual_mempty {inst_a : Type} `{GHC.Base.Monoid inst_a}
   : Dual inst_a :=
  Mk_Dual GHC.Base.mempty.

Local Definition Monoid__Dual_mconcat {inst_a : Type} `{GHC.Base.Monoid inst_a}
   : list (Dual inst_a) -> Dual inst_a :=
  GHC.Base.foldr Monoid__Dual_mappend Monoid__Dual_mempty.

Program Instance Monoid__Dual {a : Type} `{GHC.Base.Monoid a}
   : GHC.Base.Monoid (Dual a) :=
  fun _ k__ =>
    k__ {| GHC.Base.mappend__ := Monoid__Dual_mappend ;
           GHC.Base.mconcat__ := Monoid__Dual_mconcat ;
           GHC.Base.mempty__ := Monoid__Dual_mempty |}.

Local Definition Functor__Dual_fmap
   : forall {a : Type}, forall {b : Type}, (a -> b) -> Dual a -> Dual b :=
  fun {a : Type} {b : Type} => GHC.Prim.coerce.

Local Definition Functor__Dual_op_zlzd__
   : forall {a : Type}, forall {b : Type}, a -> Dual b -> Dual a :=
  fun {a : Type} {b : Type} => Functor__Dual_fmap GHC.Base.∘ GHC.Base.const.

Program Instance Functor__Dual : GHC.Base.Functor Dual :=
  fun _ k__ =>
    k__ {| GHC.Base.fmap__ := fun {a : Type} {b : Type} => Functor__Dual_fmap ;
           GHC.Base.op_zlzd____ := fun {a : Type} {b : Type} => Functor__Dual_op_zlzd__ |}.

Local Definition Applicative__Dual_op_zlztzg__
   : forall {a : Type}, forall {b : Type}, Dual (a -> b) -> Dual a -> Dual b :=
  fun {a : Type} {b : Type} => GHC.Prim.coerce.

Local Definition Applicative__Dual_liftA2
   : forall {a : Type},
     forall {b : Type},
     forall {c : Type}, (a -> b -> c) -> Dual a -> Dual b -> Dual c :=
  fun {a : Type} {b : Type} {c : Type} =>
    fun f x => Applicative__Dual_op_zlztzg__ (GHC.Base.fmap f x).

Local Definition Applicative__Dual_op_ztzg__
   : forall {a : Type}, forall {b : Type}, Dual a -> Dual b -> Dual b :=
  fun {a : Type} {b : Type} =>
    fun a1 a2 => Applicative__Dual_op_zlztzg__ (GHC.Base.id GHC.Base.<$ a1) a2.

Local Definition Applicative__Dual_pure : forall {a : Type}, a -> Dual a :=
  fun {a : Type} => Mk_Dual.

Program Instance Applicative__Dual : GHC.Base.Applicative Dual :=
  fun _ k__ =>
    k__ {| GHC.Base.liftA2__ := fun {a : Type} {b : Type} {c : Type} =>
             Applicative__Dual_liftA2 ;
           GHC.Base.op_zlztzg____ := fun {a : Type} {b : Type} =>
             Applicative__Dual_op_zlztzg__ ;
           GHC.Base.op_ztzg____ := fun {a : Type} {b : Type} =>
             Applicative__Dual_op_ztzg__ ;
           GHC.Base.pure__ := fun {a : Type} => Applicative__Dual_pure |}.

Local Definition Monad__Dual_op_zgzgze__
   : forall {a : Type}, forall {b : Type}, Dual a -> (a -> Dual b) -> Dual b :=
  fun {a : Type} {b : Type} => fun m k => k (getDual m).

Local Definition Monad__Dual_op_zgzg__
   : forall {a : Type}, forall {b : Type}, Dual a -> Dual b -> Dual b :=
  fun {a : Type} {b : Type} =>
    fun m k => Monad__Dual_op_zgzgze__ m (fun arg_0__ => k).

Local Definition Monad__Dual_return_ : forall {a : Type}, a -> Dual a :=
  fun {a : Type} => GHC.Base.pure.

Program Instance Monad__Dual : GHC.Base.Monad Dual :=
  fun _ k__ =>
    k__ {| GHC.Base.op_zgzg____ := fun {a : Type} {b : Type} =>
             Monad__Dual_op_zgzg__ ;
           GHC.Base.op_zgzgze____ := fun {a : Type} {b : Type} => Monad__Dual_op_zgzgze__ ;
           GHC.Base.return___ := fun {a : Type} => Monad__Dual_return_ |}.

Instance Unpeel_Endo a : HsToCoq.Unpeel.Unpeel (Endo a) (a -> a) :=
  HsToCoq.Unpeel.Build_Unpeel _ _ appEndo Mk_Endo.

Local Definition Semigroup__Endo_op_zlzlzgzg__ {inst_a : Type}
   : Endo inst_a -> Endo inst_a -> Endo inst_a :=
  GHC.Prim.coerce (_GHC.Base.∘_ : (inst_a -> inst_a) ->
                   (inst_a -> inst_a) -> (inst_a -> inst_a)).

Program Instance Semigroup__Endo {a : Type} : GHC.Base.Semigroup (Endo a) :=
  fun _ k__ =>
    k__ {| GHC.Base.op_zlzlzgzg____ := Semigroup__Endo_op_zlzlzgzg__ |}.

Local Definition Monoid__Endo_mappend {inst_a : Type}
   : Endo inst_a -> Endo inst_a -> Endo inst_a :=
  _GHC.Base.<<>>_.

Local Definition Monoid__Endo_mempty {inst_a : Type} : Endo inst_a :=
  Mk_Endo GHC.Base.id.

Local Definition Monoid__Endo_mconcat {inst_a : Type}
   : list (Endo inst_a) -> Endo inst_a :=
  GHC.Base.foldr Monoid__Endo_mappend Monoid__Endo_mempty.

Program Instance Monoid__Endo {a : Type} : GHC.Base.Monoid (Endo a) :=
  fun _ k__ =>
    k__ {| GHC.Base.mappend__ := Monoid__Endo_mappend ;
           GHC.Base.mconcat__ := Monoid__Endo_mconcat ;
           GHC.Base.mempty__ := Monoid__Endo_mempty |}.

Local Definition Semigroup__All_op_zlzlzgzg__ : All -> All -> All :=
  GHC.Prim.coerce andb.

Program Instance Semigroup__All : GHC.Base.Semigroup All :=
  fun _ k__ => k__ {| GHC.Base.op_zlzlzgzg____ := Semigroup__All_op_zlzlzgzg__ |}.

Local Definition Monoid__All_mappend : All -> All -> All :=
  _GHC.Base.<<>>_.

Local Definition Monoid__All_mempty : All :=
  Mk_All true.

Local Definition Monoid__All_mconcat : list All -> All :=
  GHC.Base.foldr Monoid__All_mappend Monoid__All_mempty.

Program Instance Monoid__All : GHC.Base.Monoid All :=
  fun _ k__ =>
    k__ {| GHC.Base.mappend__ := Monoid__All_mappend ;
           GHC.Base.mconcat__ := Monoid__All_mconcat ;
           GHC.Base.mempty__ := Monoid__All_mempty |}.

Local Definition Semigroup__Any_op_zlzlzgzg__ : Any -> Any -> Any :=
  GHC.Prim.coerce orb.

Program Instance Semigroup__Any : GHC.Base.Semigroup Any :=
  fun _ k__ => k__ {| GHC.Base.op_zlzlzgzg____ := Semigroup__Any_op_zlzlzgzg__ |}.

Local Definition Monoid__Any_mappend : Any -> Any -> Any :=
  _GHC.Base.<<>>_.

Local Definition Monoid__Any_mempty : Any :=
  Mk_Any false.

Local Definition Monoid__Any_mconcat : list Any -> Any :=
  GHC.Base.foldr Monoid__Any_mappend Monoid__Any_mempty.

Program Instance Monoid__Any : GHC.Base.Monoid Any :=
  fun _ k__ =>
    k__ {| GHC.Base.mappend__ := Monoid__Any_mappend ;
           GHC.Base.mconcat__ := Monoid__Any_mconcat ;
           GHC.Base.mempty__ := Monoid__Any_mempty |}.

Local Definition Semigroup__Sum_op_zlzlzgzg__ {inst_a : Type} `{GHC.Num.Num
  inst_a}
   : Sum inst_a -> Sum inst_a -> Sum inst_a :=
  GHC.Prim.coerce (_GHC.Num.+_ : inst_a -> inst_a -> inst_a).

Program Instance Semigroup__Sum {a : Type} `{GHC.Num.Num a}
   : GHC.Base.Semigroup (Sum a) :=
  fun _ k__ => k__ {| GHC.Base.op_zlzlzgzg____ := Semigroup__Sum_op_zlzlzgzg__ |}.

Local Definition Monoid__Sum_mappend {inst_a : Type} `{GHC.Num.Num inst_a}
   : Sum inst_a -> Sum inst_a -> Sum inst_a :=
  _GHC.Base.<<>>_.

Local Definition Monoid__Sum_mempty {inst_a : Type} `{GHC.Num.Num inst_a}
   : Sum inst_a :=
  Mk_Sum #0.

Local Definition Monoid__Sum_mconcat {inst_a : Type} `{GHC.Num.Num inst_a}
   : list (Sum inst_a) -> Sum inst_a :=
  GHC.Base.foldr Monoid__Sum_mappend Monoid__Sum_mempty.

Program Instance Monoid__Sum {a : Type} `{GHC.Num.Num a}
   : GHC.Base.Monoid (Sum a) :=
  fun _ k__ =>
    k__ {| GHC.Base.mappend__ := Monoid__Sum_mappend ;
           GHC.Base.mconcat__ := Monoid__Sum_mconcat ;
           GHC.Base.mempty__ := Monoid__Sum_mempty |}.

Local Definition Functor__Sum_fmap
   : forall {a : Type}, forall {b : Type}, (a -> b) -> Sum a -> Sum b :=
  fun {a : Type} {b : Type} => GHC.Prim.coerce.

Local Definition Functor__Sum_op_zlzd__
   : forall {a : Type}, forall {b : Type}, a -> Sum b -> Sum a :=
  fun {a : Type} {b : Type} => Functor__Sum_fmap GHC.Base.∘ GHC.Base.const.

Program Instance Functor__Sum : GHC.Base.Functor Sum :=
  fun _ k__ =>
    k__ {| GHC.Base.fmap__ := fun {a : Type} {b : Type} => Functor__Sum_fmap ;
           GHC.Base.op_zlzd____ := fun {a : Type} {b : Type} => Functor__Sum_op_zlzd__ |}.

Local Definition Applicative__Sum_op_zlztzg__
   : forall {a : Type}, forall {b : Type}, Sum (a -> b) -> Sum a -> Sum b :=
  fun {a : Type} {b : Type} => GHC.Prim.coerce.

Local Definition Applicative__Sum_liftA2
   : forall {a : Type},
     forall {b : Type},
     forall {c : Type}, (a -> b -> c) -> Sum a -> Sum b -> Sum c :=
  fun {a : Type} {b : Type} {c : Type} =>
    fun f x => Applicative__Sum_op_zlztzg__ (GHC.Base.fmap f x).

Local Definition Applicative__Sum_op_ztzg__
   : forall {a : Type}, forall {b : Type}, Sum a -> Sum b -> Sum b :=
  fun {a : Type} {b : Type} =>
    fun a1 a2 => Applicative__Sum_op_zlztzg__ (GHC.Base.id GHC.Base.<$ a1) a2.

Local Definition Applicative__Sum_pure : forall {a : Type}, a -> Sum a :=
  fun {a : Type} => Mk_Sum.

Program Instance Applicative__Sum : GHC.Base.Applicative Sum :=
  fun _ k__ =>
    k__ {| GHC.Base.liftA2__ := fun {a : Type} {b : Type} {c : Type} =>
             Applicative__Sum_liftA2 ;
           GHC.Base.op_zlztzg____ := fun {a : Type} {b : Type} =>
             Applicative__Sum_op_zlztzg__ ;
           GHC.Base.op_ztzg____ := fun {a : Type} {b : Type} =>
             Applicative__Sum_op_ztzg__ ;
           GHC.Base.pure__ := fun {a : Type} => Applicative__Sum_pure |}.

Local Definition Monad__Sum_op_zgzgze__
   : forall {a : Type}, forall {b : Type}, Sum a -> (a -> Sum b) -> Sum b :=
  fun {a : Type} {b : Type} => fun m k => k (getSum m).

Local Definition Monad__Sum_op_zgzg__
   : forall {a : Type}, forall {b : Type}, Sum a -> Sum b -> Sum b :=
  fun {a : Type} {b : Type} =>
    fun m k => Monad__Sum_op_zgzgze__ m (fun arg_0__ => k).

Local Definition Monad__Sum_return_ : forall {a : Type}, a -> Sum a :=
  fun {a : Type} => GHC.Base.pure.

Program Instance Monad__Sum : GHC.Base.Monad Sum :=
  fun _ k__ =>
    k__ {| GHC.Base.op_zgzg____ := fun {a : Type} {b : Type} =>
             Monad__Sum_op_zgzg__ ;
           GHC.Base.op_zgzgze____ := fun {a : Type} {b : Type} => Monad__Sum_op_zgzgze__ ;
           GHC.Base.return___ := fun {a : Type} => Monad__Sum_return_ |}.

Local Definition Semigroup__Product_op_zlzlzgzg__ {inst_a : Type} `{GHC.Num.Num
  inst_a}
   : Product inst_a -> Product inst_a -> Product inst_a :=
  GHC.Prim.coerce (_GHC.Num.*_ : inst_a -> inst_a -> inst_a).

Program Instance Semigroup__Product {a : Type} `{GHC.Num.Num a}
   : GHC.Base.Semigroup (Product a) :=
  fun _ k__ =>
    k__ {| GHC.Base.op_zlzlzgzg____ := Semigroup__Product_op_zlzlzgzg__ |}.

Local Definition Monoid__Product_mappend {inst_a : Type} `{GHC.Num.Num inst_a}
   : Product inst_a -> Product inst_a -> Product inst_a :=
  _GHC.Base.<<>>_.

Local Definition Monoid__Product_mempty {inst_a : Type} `{GHC.Num.Num inst_a}
   : Product inst_a :=
  Mk_Product #1.

Local Definition Monoid__Product_mconcat {inst_a : Type} `{GHC.Num.Num inst_a}
   : list (Product inst_a) -> Product inst_a :=
  GHC.Base.foldr Monoid__Product_mappend Monoid__Product_mempty.

Program Instance Monoid__Product {a : Type} `{GHC.Num.Num a}
   : GHC.Base.Monoid (Product a) :=
  fun _ k__ =>
    k__ {| GHC.Base.mappend__ := Monoid__Product_mappend ;
           GHC.Base.mconcat__ := Monoid__Product_mconcat ;
           GHC.Base.mempty__ := Monoid__Product_mempty |}.

Local Definition Functor__Product_fmap
   : forall {a : Type}, forall {b : Type}, (a -> b) -> Product a -> Product b :=
  fun {a : Type} {b : Type} => GHC.Prim.coerce.

Local Definition Functor__Product_op_zlzd__
   : forall {a : Type}, forall {b : Type}, a -> Product b -> Product a :=
  fun {a : Type} {b : Type} => Functor__Product_fmap GHC.Base.∘ GHC.Base.const.

Program Instance Functor__Product : GHC.Base.Functor Product :=
  fun _ k__ =>
    k__ {| GHC.Base.fmap__ := fun {a : Type} {b : Type} => Functor__Product_fmap ;
           GHC.Base.op_zlzd____ := fun {a : Type} {b : Type} =>
             Functor__Product_op_zlzd__ |}.

Local Definition Applicative__Product_op_zlztzg__
   : forall {a : Type},
     forall {b : Type}, Product (a -> b) -> Product a -> Product b :=
  fun {a : Type} {b : Type} => GHC.Prim.coerce.

Local Definition Applicative__Product_liftA2
   : forall {a : Type},
     forall {b : Type},
     forall {c : Type}, (a -> b -> c) -> Product a -> Product b -> Product c :=
  fun {a : Type} {b : Type} {c : Type} =>
    fun f x => Applicative__Product_op_zlztzg__ (GHC.Base.fmap f x).

Local Definition Applicative__Product_op_ztzg__
   : forall {a : Type}, forall {b : Type}, Product a -> Product b -> Product b :=
  fun {a : Type} {b : Type} =>
    fun a1 a2 => Applicative__Product_op_zlztzg__ (GHC.Base.id GHC.Base.<$ a1) a2.

Local Definition Applicative__Product_pure
   : forall {a : Type}, a -> Product a :=
  fun {a : Type} => Mk_Product.

Program Instance Applicative__Product : GHC.Base.Applicative Product :=
  fun _ k__ =>
    k__ {| GHC.Base.liftA2__ := fun {a : Type} {b : Type} {c : Type} =>
             Applicative__Product_liftA2 ;
           GHC.Base.op_zlztzg____ := fun {a : Type} {b : Type} =>
             Applicative__Product_op_zlztzg__ ;
           GHC.Base.op_ztzg____ := fun {a : Type} {b : Type} =>
             Applicative__Product_op_ztzg__ ;
           GHC.Base.pure__ := fun {a : Type} => Applicative__Product_pure |}.

Local Definition Monad__Product_op_zgzgze__
   : forall {a : Type},
     forall {b : Type}, Product a -> (a -> Product b) -> Product b :=
  fun {a : Type} {b : Type} => fun m k => k (getProduct m).

Local Definition Monad__Product_op_zgzg__
   : forall {a : Type}, forall {b : Type}, Product a -> Product b -> Product b :=
  fun {a : Type} {b : Type} =>
    fun m k => Monad__Product_op_zgzgze__ m (fun arg_0__ => k).

Local Definition Monad__Product_return_ : forall {a : Type}, a -> Product a :=
  fun {a : Type} => GHC.Base.pure.

Program Instance Monad__Product : GHC.Base.Monad Product :=
  fun _ k__ =>
    k__ {| GHC.Base.op_zgzg____ := fun {a : Type} {b : Type} =>
             Monad__Product_op_zgzg__ ;
           GHC.Base.op_zgzgze____ := fun {a : Type} {b : Type} =>
             Monad__Product_op_zgzgze__ ;
           GHC.Base.return___ := fun {a : Type} => Monad__Product_return_ |}.

(* Skipping instance `Data.SemigroupInternal.Semigroup__Alt' of class
   `GHC.Base.Semigroup' *)

(* Skipping instance `Data.SemigroupInternal.Monoid__Alt' of class
   `GHC.Base.Monoid' *)

(* Skipping definition `Data.SemigroupInternal.stimesIdempotent' *)

Definition stimesIdempotentMonoid {b : Type} {a : Type} `{GHC.Real.Integral b}
  `{GHC.Base.Monoid a}
   : b -> a -> a :=
  fun n x =>
    match GHC.Base.compare n #0 with
    | Lt =>
        GHC.Err.errorWithoutStackTrace (GHC.Base.hs_string__
                                        "stimesIdempotentMonoid: negative multiplier")
    | Eq => GHC.Base.mempty
    | Gt => x
    end.

(* Skipping definition `Data.SemigroupInternal.stimesMonoid' *)

(* Skipping definition `Data.SemigroupInternal.stimesDefault' *)

(* Skipping definition `Data.SemigroupInternal.stimesMaybe' *)

(* Skipping definition `Data.SemigroupInternal.stimesList' *)

(* External variables:
     Eq Gt Lt Type andb bool comparison false list orb true GHC.Base.Applicative
     GHC.Base.Eq_ GHC.Base.Functor GHC.Base.Monad GHC.Base.Monoid GHC.Base.Ord
     GHC.Base.Semigroup GHC.Base.compare GHC.Base.compare__ GHC.Base.const
     GHC.Base.fmap GHC.Base.fmap__ GHC.Base.foldr GHC.Base.id GHC.Base.liftA2
     GHC.Base.liftA2__ GHC.Base.mappend__ GHC.Base.max GHC.Base.max__
     GHC.Base.mconcat__ GHC.Base.mempty GHC.Base.mempty__ GHC.Base.min GHC.Base.min__
     GHC.Base.op_z2218U__ GHC.Base.op_zeze__ GHC.Base.op_zeze____ GHC.Base.op_zg__
     GHC.Base.op_zg____ GHC.Base.op_zgze__ GHC.Base.op_zgze____ GHC.Base.op_zgzg__
     GHC.Base.op_zgzg____ GHC.Base.op_zgzgze__ GHC.Base.op_zgzgze____
     GHC.Base.op_zl__ GHC.Base.op_zl____ GHC.Base.op_zlzd__ GHC.Base.op_zlzd____
     GHC.Base.op_zlze__ GHC.Base.op_zlze____ GHC.Base.op_zlzlzgzg__
     GHC.Base.op_zlzlzgzg____ GHC.Base.op_zlztzg__ GHC.Base.op_zlztzg____
     GHC.Base.op_zsze__ GHC.Base.op_zsze____ GHC.Base.op_ztzg__ GHC.Base.op_ztzg____
     GHC.Base.pure GHC.Base.pure__ GHC.Base.return_ GHC.Base.return___
     GHC.Err.errorWithoutStackTrace GHC.Num.Num GHC.Num.fromInteger GHC.Num.op_zp__
     GHC.Num.op_zt__ GHC.Prim.coerce GHC.Real.Integral HsToCoq.Err.Build_Default
     HsToCoq.Err.Default HsToCoq.Err.default HsToCoq.Unpeel.Build_Unpeel
     HsToCoq.Unpeel.Unpeel
*)

author: plclub

repo: hs-to-coq

save_path: github-repos/coq/plclub-hs-to-coq


text:
(** * Mapping predicates over [StringLike] things *)
Require Import Coq.Classes.Morphisms Coq.Classes.RelationClasses Coq.Program.Basics.
Require Import Coq.omega.Omega.
Require Import Coq.Numbers.Natural.Peano.NPeano.
Require Import Fiat.Parsers.StringLike.Core.
Require Import Fiat.Parsers.StringLike.Properties.
Require Import Fiat.Common.

Set Implicit Arguments.
Local Open Scope string_like_scope.

Section forall_chars.
  Context {Char} {HSLM : StringLikeMin Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char}.

  Definition forall_chars (str : String) (P : Char -> Prop)
    := forall n ch,
         take 1 (drop n str) ~= [ ch ]
         -> P ch.

  Lemma forall_chars_from_get (str : String) (P : Char -> Prop)
  : (forall n ch, get n str = Some ch -> P ch) -> forall_chars str P.
  Proof.
    unfold forall_chars.
    intros H n ch Heq.
    apply (H n); clear H.
    rewrite get_drop, <- get_0; assumption.
  Qed.

  Global Instance forall_chars_Proper
  : Proper (beq ==> pointwise_relation _ impl ==> impl) forall_chars.
  Proof.
    unfold pointwise_relation, respectful, forall_chars, impl.
    intros ?? H' ?? H'' H''' ?? H.
    rewrite <- H' in H.
    eauto using is_char_Proper.
  Qed.

  Global Instance forall_chars_Proper_flip
  : Proper (beq ==> pointwise_relation _ (flip impl) ==> flip impl) forall_chars.
  Proof.
    unfold pointwise_relation, respectful, forall_chars, flip, impl.
    intros ?? H' ?? H'' H''' ?? H.
    rewrite H' in H.
    eauto using is_char_Proper.
  Qed.

  Global Instance forall_chars_Proper_iff
  : Proper (beq ==> pointwise_relation _ iff ==> iff) forall_chars.
  Proof.
    unfold pointwise_relation, respectful.
    repeat intro; split;
    apply forall_chars_Proper; try assumption; repeat intro;
    match goal with
      | [ H : _ |- _ ] => apply H; assumption
    end.
  Qed.

  Lemma forall_chars_nil (str : String) P
  : length str = 0 -> forall_chars str P.
  Proof.
    intros H n ch H'.
    apply length_singleton in H'.
    rewrite take_length, drop_length, H in H'.
    simpl in H'; omega.
  Qed.

  Lemma helper
        (P : nat -> nat -> Type)
        n
        (H0 : forall n0, P (min 1 (n - n0)) n0)
        (H1 : forall n0, P 1 (n0 + n))
        {n0}
  : P 1 n0.
  Proof.
    destruct (Compare_dec.le_dec n n0) as [H'|H'].
    { specialize (H1 (n0 - n)).
      rewrite Nat.sub_add in H1 by assumption; assumption. }
    { apply Compare_dec.not_le in H'.
      specialize (H0 n0).
      destruct (n - n0) as [|[|]] eqn:?; simpl in *; trivial; omega. }
  Defined.

  Lemma forall_chars__split (str : String) P n
  : forall_chars str P
    <-> (forall_chars (take n str) P /\ forall_chars (drop n str) P).
  Proof.
    unfold forall_chars; repeat (split || intro);
    repeat match goal with
                         | [ H : _ |- _ ] => setoid_rewrite drop_length in H
                         | [ H : _ |- _ ] => setoid_rewrite take_length in H
                         | [ H : _ |- _ ] => setoid_rewrite drop_take in H
                         | [ H : _ |- _ ] => setoid_rewrite take_take in H
                         | [ H : _ |- _ ] => setoid_rewrite drop_drop in H
                         | [ H : _ /\ _ |- _ ] => destruct H
                         | [ H : context[min 1 ?x] |- _ ] => destruct x eqn:?; simpl in H
                         | [ H : is_true (take 0 _ ~= [ _ ]) |- _ ] => exfalso; apply length_singleton in H
                         | _ => omega
                         | _ => progress simpl in *; omega
                         | _ => solve [ eauto ]
                         | _ => solve [ eapply (@helper (fun a b => take a (drop b str) ~= [ ch ] -> P ch)); eauto ]
                       end.
  Qed.

  Lemma forall_chars_singleton (str : String) P ch
  : str ~= [ ch ] -> (P ch <-> forall_chars str P).
  Proof.
    intro H.
    pose proof (length_singleton _ _ H).
    unfold forall_chars.
    split; intro H'; repeat intro.
    { match goal with
        | [ n : nat |- _ ] => destruct n; [ | exfalso ]
      end;
      repeat match goal with
               | _ => intro
               | _ => omega
               | [ H : _ |- _ ] => rewrite drop_0 in H
               | [ H : _, H' : _ |- _ ] => rewrite (singleton_take H') in H
               | [ H : _ |- False ] => apply length_singleton in H
               | [ H : _ |- _ ] => rewrite take_length in H
               | [ H : _ |- _ ] => rewrite drop_length in H
               | [ H : ?x = 1, H' : context[?x] |- _ ] => rewrite H in H'
               | _ => erewrite singleton_unique; eassumption
               | [ H : appcontext[min] |- _ ] => revert H; apply Min.min_case_strong
             end. }
    { match goal with
        | [ H : _ |- _ ] => apply (H 0)
      end.
      rewrite drop_0.
      rewrite take_long; trivial; omega. }
  Qed.

  Lemma forall_chars_singleton_length (str : String) P (H : length str = 1)
  : forall_chars str P <-> (forall ch, str ~= [ ch ] -> P ch).
  Proof.
    split.
    { intro H''.
      intros ch' H'''.
      apply (forall_chars_singleton _ _ _ H'''); assumption. }
    { destruct (singleton_exists _ H) as [ch H'].
      intro H''.
      apply (forall_chars_singleton _ P ch H'); eauto. }
  Qed.

  Lemma forall_chars_False (str : String) P
  : (forall ch, ~P ch) -> forall_chars str P -> length str = 0.
  Proof.
    intros H' H.
    case_eq (length str); trivial.
    specialize (H (length str - 1)).
    pose proof (singleton_exists (drop (length str - 1) str)) as H''.
    rewrite drop_length in H''.
    intros n H'''.
    rewrite H''' in *.
    rewrite sub_plus in H'' by omega.
    rewrite Minus.minus_diag in *.
    specialize (H'' eq_refl).
    destruct H'' as [ch H''].
    exfalso; eapply H', H.
    rewrite take_long; try eassumption.
    apply length_singleton in H''; omega.
  Qed.

  Global Opaque forall_chars.

  Lemma forall_chars__split_forall (str : String) P
  : forall_chars str P
    <-> (forall n, forall_chars (take n str) P /\ forall_chars (drop n str) P).
  Proof.
    split.
    { intros H n.
      rewrite <- forall_chars__split; assumption. }
    { intro H.
      specialize (H 0).
      rewrite forall_chars__split; eassumption. }
  Qed.

  Lemma forall_chars_take (str : String) P
  : forall_chars str P <-> (forall n, forall_chars (take (S n) str) P).
  Proof.
    split.
    { intros H n.
      revert H; rewrite forall_chars__split; intro H; destruct H; eassumption. }
    { intro H.
      specialize (H (length str)).
      rewrite take_long in H by omega; assumption. }
  Qed.

  Lemma forall_chars_drop (str : String) P
  : forall_chars str P <-> (forall n, forall_chars (drop n str) P).
  Proof.
    split.
    { intros H n.
      revert H; rewrite forall_chars__split; intro H; destruct H; eassumption. }
    { intro H.
      specialize (H 0).
      rewrite drop_0 in H; assumption. }
  Qed.

  Lemma forall_chars_get (str : String) P
  : forall_chars str P <-> (forall n ch, get n str = Some ch -> P ch).
  Proof.
    split.
    { intros H n ch Heq.
      rewrite get_drop in Heq.
      apply get_0 in Heq.
      apply forall_chars__split with (n := n) in H.
      destruct H as [_ H].
      apply forall_chars__split with (n := 1) in H.
      destruct H as [H _].
      rewrite forall_chars_singleton_length in H.
      { auto. }
      { apply length_singleton in Heq; assumption. } }
    { apply forall_chars_from_get. }
  Qed.

  Definition forall_chars__char_in (str : String) (ls : list Char)
    := forall_chars str (fun ch => List.In ch ls).

  Definition forall_chars__impl__forall_chars__char_in {str ls} {P : _ -> Prop}
             (H : forall ch, P ch -> List.In ch ls)
  : impl (forall_chars str P) (forall_chars__char_in str ls).
  Proof.
    unfold forall_chars__char_in.
    apply forall_chars_Proper; trivial; reflexivity.
  Qed.

  Definition forall_chars__char_in__impl__forall_chars {str ls} {P : _ -> Prop}
             (H : forall ch, List.In ch ls -> P ch)
  : impl (forall_chars__char_in str ls) (forall_chars str P).
  Proof.
    unfold forall_chars__char_in.
    apply forall_chars_Proper; trivial; reflexivity.
  Qed.

  Global Instance forall_chars__char_in__Proper
  : Proper (beq ==> eq ==> impl) forall_chars__char_in.
  Proof.
    unfold pointwise_relation, respectful, forall_chars__char_in, impl.
    repeat intro; subst.
    match goal with
      | [ H : _ |- _ ] => rewrite <- H; assumption
    end.
  Qed.

  Global Instance forall_chars__char_in__Proper_iff
  : Proper (beq ==> eq ==> iff) forall_chars__char_in.
  Proof.
    unfold pointwise_relation, respectful, forall_chars__char_in, impl.
    repeat intro; subst.
    match goal with
      | [ H : _ |- _ ] => rewrite <- H; reflexivity
    end.
  Qed.

  Lemma forall_chars__char_in__split n (str : String) ls
  : forall_chars__char_in str ls
    <-> (forall_chars__char_in (take n str) ls /\ forall_chars__char_in (drop n str) ls).
  Proof.
    unfold forall_chars__char_in; apply forall_chars__split.
  Qed.

  Lemma forall_chars__char_in__app_or_iff (str : String) (ls1 ls2 : list Char)
  : forall_chars__char_in str (ls1 ++ ls2)
    <-> (forall_chars str (fun ch => List.In ch ls1 \/ List.In ch ls2)).
  Proof.
    unfold forall_chars__char_in; split; repeat intro.
    { eapply forall_chars_Proper; [ .. | eassumption ]; [ reflexivity | ].
      intro; hnf.
      apply List.in_app_or. }
    { eapply forall_chars_Proper; [ .. | eassumption ]; [ reflexivity | ].
      intro; hnf.
      apply List.in_or_app. }
  Qed.

  Lemma forall_chars__char_in__or_app (str : String) (ls1 ls2 : list Char)
  : forall_chars__char_in str ls1 \/ forall_chars__char_in str ls2 -> forall_chars__char_in str (ls1 ++ ls2).
  Proof.
    unfold forall_chars__char_in.
    intros [?|?]; repeat intro;
    (eapply forall_chars_Proper; [ .. | eassumption ]; [ reflexivity | ]; intros ??);
    apply List.in_or_app; eauto.
  Qed.

  Lemma forall_chars__char_in_nil (str : String)
  : forall_chars__char_in str nil <-> length str = 0.
  Proof.
    unfold forall_chars__char_in.
    split.
    { eapply forall_chars_False; simpl; eauto. }
    { apply forall_chars_nil. }
  Qed.

  Lemma forall_chars__char_in_empty (str : String) (H : length str = 0) ls
  : forall_chars__char_in str ls.
  Proof.
    unfold forall_chars__char_in.
    apply forall_chars_nil; assumption.
  Qed.

  Lemma forall_chars__char_in_singleton_str (str : String) ls ch (H : str ~= [ ch ])
  : forall_chars__char_in str ls <-> List.In ch ls.
  Proof.
    unfold forall_chars__char_in.
    rewrite <- forall_chars_singleton; try eassumption; reflexivity.
  Qed.

  Global Opaque forall_chars__char_in.
End forall_chars.

author: JasonGross

repo: slow-coq-examples


text:
(*
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 * http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 *)

Require Import String.
Require Import List.
Require Import Sorting.Mergesort.
Require Import EquivDec.
Require Import Utils.
Require Import DataRuntime.
Require Import ForeignReduceOps.
Require Import ForeignToReduceOps.
Require Import NNRCSystem.
Require Import NNRCMRSystem.
Require Import DNNRCSystem.
Require Import NNRCtoDNNRC.

Section NNRCMRtoDNNRC.
  Local Open Scope string_scope.

  Context {fruntime:foreign_runtime}.
  Context {fredop:foreign_reduce_op}.
  Context {ftoredop:foreign_to_reduce_op}.

  Context (h:list(string*string)).

  Context {A plug_type:Set}.

  Definition map_res_id (mr_id: string) :=
    "mapRes_"++mr_id.

  (* Generates the DNNRC code corresponding to "(fun x => e1) e2" that is:
       let x = e2 in e1
   *)
  Definition gen_apply_fun (annot:A) (f: var * nnrc) (e2: @dnnrc_base _ A plug_type) : (@dnnrc_base _ A plug_type) :=
    let (x, e1) := f in
    DNNRCLet annot
            x e2
            (nnrc_to_dnnrc_base annot nil ((x, Vlocal)::nil) e1).

  (* Generates the DNNRC code corresponding to "(fun (x1, ..., xn) => e) (e1, ..., en)" that is:
       let x1 = e1 in
       ...
       let xn = en in
       e
   *)
  Definition gen_apply_fun_n (annot:A) (f: list var * nnrc)  (eff: list (var * dlocalization)) : option (@dnnrc_base _ A plug_type) :=
    let (form, e) := f in
    match zip form eff with
    | Some l =>
      let form_loc :=
          List.map
            (fun t =>
               let '(x, (y, loc)) := t in
               (x, loc))
            l
      in
      Some
        (List.fold_right
           (fun t k =>
              let '(x, (y, loc)) := t in
              DNNRCLet annot
                      x (DNNRCVar annot y)
                      k)
           (nnrc_to_dnnrc_base annot form_loc nil e)
           l)
    | None => None
    end.

  Definition dnnrc_base_distr_of_mr_map (annot:A) (input: var) (mr_map: map_fun) : (@dnnrc_base _ A plug_type) :=
    match mr_map with
    | MapDist (x, n) =>
      DNNRCFor annot x (DNNRCVar annot input) (nnrc_to_dnnrc_base annot nil ((x, Vlocal)::nil) n)
    | MapDistFlatten (x, n) =>
      let res_map :=
          DNNRCFor annot x (DNNRCVar annot input) (nnrc_to_dnnrc_base annot nil ((x, Vlocal)::nil) n)
      in
      DNNRCUnop annot OpFlatten res_map
    | MapScalar (x, n) =>
      let distr_input := DNNRCDispatch annot (DNNRCVar annot input) in
      DNNRCFor annot x distr_input (nnrc_to_dnnrc_base annot nil ((x, Vlocal)::nil) n)
    end.

  Definition dnnrc_base_local_of_mr_map (annot:A) (input: var) (mr_map: map_fun) : (@dnnrc_base _ A plug_type) :=
    match mr_map with
    | MapDist (x, n) =>
      let res_map := DNNRCFor annot x (DNNRCVar annot input) (nnrc_to_dnnrc_base annot nil ((x, Vlocal)::nil) n) in
      DNNRCCollect annot res_map
    | MapDistFlatten (x, n) =>
      let res_map := DNNRCFor annot x (DNNRCVar annot input) (nnrc_to_dnnrc_base annot nil ((x, Vlocal)::nil) n) in
      DNNRCCollect annot (DNNRCUnop annot OpFlatten res_map)
    | MapScalar (x, n) =>
      DNNRCFor annot x (DNNRCVar annot input) (nnrc_to_dnnrc_base annot nil ((x, Vlocal)::nil) n)
    end.

  Definition dnnrc_base_of_mr (annot:A) (m:mr) : option (@dnnrc_base _ A plug_type) :=
    match (m.(mr_map), m.(mr_reduce)) with
    | (MapScalar (x, NNRCUnop OpBag n), RedSingleton) =>
      Some (gen_apply_fun annot (x, n) (DNNRCVar annot m.(mr_input)))
    | (_, RedSingleton) =>
      None
    | (map, RedId) =>
      Some (dnnrc_base_distr_of_mr_map annot (mr_input m) map)
    | (map, RedCollect red_fun) =>
      let map_expr := dnnrc_base_local_of_mr_map annot (mr_input m) map in
      Some (gen_apply_fun annot red_fun map_expr)
    | (map, RedOp op) =>
      match op with
      | RedOpForeign frop =>
        let map_expr := dnnrc_base_distr_of_mr_map annot (mr_input m) map in
        lift (fun op => DNNRCUnop annot op map_expr) (foreign_to_reduce_op_to_unary_op op)
      end
    end.

  Fixpoint dnnrc_base_of_mr_chain (annot: A) (outputs: list var) (l: list mr) (k: @dnnrc_base _ A plug_type) : option (@dnnrc_base _ A plug_type) :=
    match l with
    | nil => Some k
    | mr :: l =>
      match (dnnrc_base_of_mr annot mr, dnnrc_base_of_mr_chain annot (mr_output mr :: outputs) l k) with
      | (Some n, Some k) =>
        Some (DNNRCLet annot
                      (mr_output mr)
                      (if in_dec equiv_dec (mr_output mr) outputs then
                         DNNRCBinop annot OpBagUnion (DNNRCVar annot (mr_output mr)) n
                       else n)
                      k)
      | _ => None
      end
    end.

  Definition dnnrc_base_of_nnrcmr_top (annot: A) (l: nnrcmr) : option (@dnnrc_base _ A plug_type) :=
    let constants := map fst (mr_inputs_loc l) in
    let (last_fun, last_args) :=  mr_last l in
    let k := gen_apply_fun_n annot last_fun last_args in
    lift (dnnrc_base_subst_var_to_const constants)
         (olift (dnnrc_base_of_mr_chain annot nil (mr_chain l)) k).

End NNRCMRtoDNNRC.

author: querycert

repo: qcert

save_path: github-repos/coq/querycert-qcert


text:
(** * Poly: Polymorphism and Higher-Order Functions *)

(** In this chapter we continue our development of basic
    concepts of functional programming.  The critical new ideas are
    _polymorphism_ (abstracting functions over the types of the data
    they manipulate) and _higher-order functions_ (treating functions
    as data).
*)

Require Export Lists.

Set Asymmetric Patterns.
(* ###################################################### *)
(** * Polymorphism *)
(* ###################################################### *)
(** ** Polymorphic Lists *)

(** For the last couple of chapters, we've been working just
    with lists of numbers.  Obviously, interesting programs also need
    to be able to manipulate lists with elements from other types --
    lists of strings, lists of booleans, lists of lists, etc.  We
    _could_ just define a new inductive datatype for each of these,
    for example... *)

Inductive boollist : Type :=
  | bool_nil : boollist
  | bool_cons : bool -> boollist -> boollist.

(** ... but this would quickly become tedious, partly because we
    have to make up different constructor names for each datatype, but
    mostly because we would also need to define new versions of all
    our list manipulating functions ([length], [rev], etc.)  for each
    new datatype definition. *)

(** *** *)

(** To avoid all this repetition, Coq supports _polymorphic_
    inductive type definitions.  For example, here is a _polymorphic
    list_ datatype. *)

Inductive list (X:Type) : Type :=
  | nil : list X
  | cons : X -> list X -> list X.

(** This is exactly like the definition of [natlist] from the
    previous chapter, except that the [nat] argument to the [cons]
    constructor has been replaced by an arbitrary type [X], a binding
    for [X] has been added to the header, and the occurrences of
    [natlist] in the types of the constructors have been replaced by
    [list X].  (We can re-use the constructor names [nil] and [cons]
    because the earlier definition of [natlist] was inside of a
    [Module] definition that is now out of scope.) *)

(** What sort of thing is [list] itself?  One good way to think
    about it is that [list] is a _function_ from [Type]s to
    [Inductive] definitions; or, to put it another way, [list] is a
    function from [Type]s to [Type]s.  For any particular type [X],
    the type [list X] is an [Inductive]ly defined set of lists whose
    elements are things of type [X]. *)

(** With this definition, when we use the constructors [nil] and
    [cons] to build lists, we need to tell Coq the type of the
    elements in the lists we are building -- that is, [nil] and [cons]
    are now _polymorphic constructors_.  Observe the types of these
    constructors: *)

Check nil.
(* ===> nil : forall X : Type, list X *)
Check cons.
(* ===> cons : forall X : Type, X -> list X -> list X *)

(** The "[forall X]" in these types can be read as an additional
    argument to the constructors that determines the expected types of
    the arguments that follow.  When [nil] and [cons] are used, these
    arguments are supplied in the same way as the others.  For
    example, the list containing [2] and [1] is written like this: *)

Check (cons nat 2 (cons nat 1 (nil nat))).

(** (We've gone back to writing [nil] and [cons] explicitly here
    because we haven't yet defined the [ [] ] and [::] notations for
    the new version of lists.  We'll do that in a bit.) *)

(** We can now go back and make polymorphic (or "generic")
    versions of all the list-processing functions that we wrote
    before.  Here is [length], for example: *)

(** *** *)
Fixpoint length (X:Type) (l:list X) : nat :=
  match l with
  | nil      => 0
  | cons h t => S (length X t)
  end.

(** Note that the uses of [nil] and [cons] in [match] patterns
    do not require any type annotations: Coq already knows that the list
    [l] contains elements of type [X], so there's no reason to include
    [X] in the pattern.  (More precisely, the type [X] is a parameter
    of the whole definition of [list], not of the individual
    constructors.  We'll come back to this point later.)

    As with [nil] and [cons], we can use [length] by applying it first
    to a type and then to its list argument: *)

Example test_length1 :
    length nat (cons nat 1 (cons nat 2 (nil nat))) = 2.
Proof. reflexivity.  Qed.

(** To use our length with other kinds of lists, we simply
    instantiate it with an appropriate type parameter: *)

Example test_length2 :
    length bool (cons bool true (nil bool)) = 1.
Proof. reflexivity.  Qed.

(** *** *)
(** Let's close this subsection by re-implementing a few other
    standard list functions on our new polymorphic lists: *)

Fixpoint app (X : Type) (l1 l2 : list X)
                : (list X) :=
  match l1 with
  | nil      => l2
  | cons h t => cons X h (app X t l2)
  end.

Fixpoint snoc (X:Type) (l:list X) (v:X) : (list X) :=
  match l with
  | nil      => cons X v (nil X)
  | cons h t => cons X h (snoc X t v)
  end.

Fixpoint rev (X:Type) (l:list X) : list X :=
  match l with
  | nil      => nil X
  | cons h t => snoc X (rev X t) h
  end.

Example test_rev1 :
    rev nat (cons nat 1 (cons nat 2 (nil nat)))
  = (cons nat 2 (cons nat 1 (nil nat))).
Proof. reflexivity.  Qed.

Example test_rev2:
  rev bool (nil bool) = nil bool.
Proof. reflexivity.  Qed.

Module MumbleBaz.
(** **** Exercise: 2 stars (mumble_grumble)  *)
(** Consider the following two inductively defined types. *)

Inductive mumble : Type :=
  | a : mumble
  | b : mumble -> nat -> mumble
  | c : mumble.
Inductive grumble (X:Type) : Type :=
  | d : mumble -> grumble X
  | e : X -> grumble X.

(** Which of the following are well-typed elements of [grumble X] for
    some type [X]?
      - [d (b a 5)]
      - [d mumble (b a 5)]
      - [d bool (b a 5)]
      - [e bool true]
      - [e mumble (b c 0)]
      - [e bool (b c 0)]
      - [c]

  + [d mumble (b a 5)]
  + [d bool (b a 5)]
  + [e bool true]
  + [e mumble (b c 0)]
*)
(** [] *)

(** **** Exercise: 2 stars (baz_num_elts)  *)
(** Consider the following inductive definition: *)

Inductive baz : Type :=
   | x : baz -> baz
   | y : baz -> bool -> baz.

(** How _many_ elements does the type [baz] have?
Zero. No base case :(
*)
(** [] *)

End MumbleBaz.

(* ###################################################### *)
(** *** Type Annotation Inference *)

(** Let's write the definition of [app] again, but this time we won't
    specify the types of any of the arguments. Will Coq still accept
    it? *)

Fixpoint app' X l1 l2 : list X :=
  match l1 with
  | nil      => l2
  | cons h t => cons X h (app' X t l2)
  end.

(** Indeed it will.  Let's see what type Coq has assigned to [app']: *)

Check app'.
(* ===> forall X : Type, list X -> list X -> list X *)
Check app.
(* ===> forall X : Type, list X -> list X -> list X *)

(** It has exactly the same type type as [app].  Coq was able to
    use a process called _type inference_ to deduce what the types of
    [X], [l1], and [l2] must be, based on how they are used.  For
    example, since [X] is used as an argument to [cons], it must be a
    [Type], since [cons] expects a [Type] as its first argument;
    matching [l1] with [nil] and [cons] means it must be a [list]; and
    so on.

    This powerful facility means we don't always have to write
    explicit type annotations everywhere, although explicit type
    annotations are still quite useful as documentation and sanity
    checks.  You should try to find a balance in your own code between
    too many type annotations (so many that they clutter and distract)
    and too few (which forces readers to perform type inference in
    their heads in order to understand your code). *)

(* ###################################################### *)
(** *** Type Argument Synthesis *)

(** Whenever we use a polymorphic function, we need to pass it
    one or more types in addition to its other arguments.  For
    example, the recursive call in the body of the [length] function
    above must pass along the type [X].  But just like providing
    explicit type annotations everywhere, this is heavy and verbose.
    Since the second argument to [length] is a list of [X]s, it seems
    entirely obvious that the first argument can only be [X] -- why
    should we have to write it explicitly?

    Fortunately, Coq permits us to avoid this kind of redundancy.  In
    place of any type argument we can write the "implicit argument"
    [_], which can be read as "Please figure out for yourself what
    type belongs here."  More precisely, when Coq encounters a [_], it
    will attempt to _unify_ all locally available information -- the
    type of the function being applied, the types of the other
    arguments, and the type expected by the context in which the
    application appears -- to determine what concrete type should
    replace the [_].

    This may sound similar to type annotation inference -- and,
    indeed, the two procedures rely on the same underlying mechanisms.
    Instead of simply omitting the types of some arguments to a
    function, like
      app' X l1 l2 : list X :=
    we can also replace the types with [_], like
      app' (X : _) (l1 l2 : _) : list X :=
    which tells Coq to attempt to infer the missing information, just
    as with argument synthesis.

    Using implicit arguments, the [length] function can be written
    like this: *)

Fixpoint length' (X:Type) (l:list X) : nat :=
  match l with
  | nil      => 0
  | cons h t => S (length' _ t)
  end.

(** In this instance, we don't save much by writing [_] instead of
    [X].  But in many cases the difference can be significant.  For
    example, suppose we want to write down a list containing the
    numbers [1], [2], and [3].  Instead of writing this... *)

Definition list123 :=
  cons nat 1 (cons nat 2 (cons nat 3 (nil nat))).

(** ...we can use argument synthesis to write this: *)

Definition list123' := cons _ 1 (cons _ 2 (cons _ 3 (nil _))).

(* ###################################################### *)
(** *** Implicit Arguments *)

(** In fact, we can go further.  To avoid having to sprinkle [_]'s
    throughout our programs, we can tell Coq _always_ to infer the
    type argument(s) of a given function. The [Arguments] directive
    specifies the name of the function or constructor, and then lists
    its argument names, with curly braces around any arguments to be
    treated as implicit.
    *)

Arguments nil {X}.
Arguments cons {X} _ _.  (* use underscore for argument position that has no name *)
Arguments length {X} l.
Arguments app {X} l1 l2.
Arguments rev {X} l.
Arguments snoc {X} l v.

(* note: no _ arguments required... *)
Definition list123'' := cons 1 (cons 2 (cons 3 nil)).
Check (length list123'').

(** *** *)

(** Alternatively, we can declare an argument to be implicit while
    defining the function itself, by surrounding the argument in curly
    braces.  For example: *)

Fixpoint length'' {X:Type} (l:list X) : nat :=
  match l with
  | nil      => 0
  | cons h t => S (length'' t)
  end.

(** (Note that we didn't even have to provide a type argument to
    the recursive call to [length'']; indeed, it is invalid to provide
    one.)  We will use this style whenever possible, although we will
    continue to use use explicit [Argument] declarations for
    [Inductive] constructors. *)

(** *** *)

(** One small problem with declaring arguments [Implicit] is
    that, occasionally, Coq does not have enough local information to
    determine a type argument; in such cases, we need to tell Coq that
    we want to give the argument explicitly this time, even though
    we've globally declared it to be [Implicit].  For example, suppose we
    write this: *)

(* Definition mynil := nil.  *)

(** If we uncomment this definition, Coq will give us an error,
    because it doesn't know what type argument to supply to [nil].  We
    can help it by providing an explicit type declaration (so that Coq
    has more information available when it gets to the "application"
    of [nil]): *)

Definition mynil : list nat := nil.

(** Alternatively, we can force the implicit arguments to be explicit by
   prefixing the function name with [@]. *)

Check @nil.

Definition mynil' := @nil nat.

(** *** *)
(** Using argument synthesis and implicit arguments, we can
    define convenient notation for lists, as before.  Since we have
    made the constructor type arguments implicit, Coq will know to
    automatically infer these when we use the notations. *)

Notation "x :: y" := (cons x y)
                     (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y []) ..).
Notation "x ++ y" := (app x y)
                     (at level 60, right associativity).

(** Now lists can be written just the way we'd hope: *)

Definition list123''' := [1; 2; 3].

(* ###################################################### *)
(** *** Exercises: Polymorphic Lists *)

(** **** Exercise: 2 stars, optional (poly_exercises)  *)
(** Here are a few simple exercises, just like ones in the [Lists]
    chapter, for practice with polymorphism.  Fill in the definitions
    and complete the proofs below. *)

Fixpoint repeat {X : Type} (n : X) (count : nat) : list X :=
  match count with
  | O => nil
  | S count' => n :: repeat n count'
  end.

Example test_repeat1:
  repeat true 2 = cons true (cons true nil).
Proof. reflexivity.  Qed.

Theorem nil_app : forall X:Type, forall l:list X,
  app [] l = l.
Proof.
  reflexivity.  Qed.

Theorem rev_snoc : forall X : Type,
                     forall v : X,
                     forall s : list X,
  rev (snoc s v) = v :: (rev s).
Proof.
  intros X v s. induction s as [| h s'].
  Case "s = []".
    reflexivity.
  Case "s = h :: s'".
    simpl. rewrite IHs'. reflexivity.  Qed.

Theorem rev_involutive : forall X : Type, forall l : list X,
  rev (rev l) = l.
Proof.
  intros X l. induction l as [| h l'].
  Case "l = []".
    reflexivity.
  Case "l = h :: l'".
    simpl. rewrite rev_snoc. rewrite IHl'. reflexivity.  Qed.

Theorem snoc_with_append : forall X : Type,
                         forall l1 l2 : list X,
                         forall v : X,
  snoc (l1 ++ l2) v = l1 ++ (snoc l2 v).
Proof.
  intros X l1 l2 v. induction l1 as [| h1 l1'].
  Case "l1 = []".
    reflexivity.
  Case "l1 = h1 :: l1'".
    simpl. rewrite IHl1'. reflexivity.  Qed.
(** [] *)

(* ###################################################### *)
(** ** Polymorphic Pairs *)

(** Following the same pattern, the type definition we gave in
    the last chapter for pairs of numbers can be generalized to
    _polymorphic pairs_ (or _products_): *)

Inductive prod (X Y : Type) : Type :=
  pair : X -> Y -> prod X Y.

Arguments pair {X} {Y} _ _.

(** As with lists, we make the type arguments implicit and define the
    familiar concrete notation. *)

Notation "( x , y )" := (pair x y).

(** We can also use the [Notation] mechanism to define the standard
    notation for pair _types_: *)

Notation "X * Y" := (prod X Y) : type_scope.

(** (The annotation [: type_scope] tells Coq that this abbreviation
    should be used when parsing types.  This avoids a clash with the
    multiplication symbol.) *)

(** *** *)
(** A note of caution: it is easy at first to get [(x,y)] and
    [X*Y] confused.  Remember that [(x,y)] is a _value_ built from two
    other values; [X*Y] is a _type_ built from two other types.  If
    [x] has type [X] and [y] has type [Y], then [(x,y)] has type
    [X*Y]. *)

(** The first and second projection functions now look pretty
    much as they would in any functional programming language. *)

Definition fst {X Y : Type} (p : X * Y) : X :=
  match p with (x,y) => x end.

Definition snd {X Y : Type} (p : X * Y) : Y :=
  match p with (x,y) => y end.

(** The following function takes two lists and combines them
    into a list of pairs.  In many functional programming languages,
    it is called [zip].  We call it [combine] for consistency with
    Coq's standard library. *)
(** Note that the pair notation can be used both in expressions and in
    patterns... *)

Fixpoint combine {X Y : Type} (lx : list X) (ly : list Y)
           : list (X*Y) :=
  match (lx,ly) with
  | ([],_) => []
  | (_,[]) => []
  | (x::tx, y::ty) => (x,y) :: (combine tx ty)
  end.

(** **** Exercise: 1 star, optional (combine_checks)  *)
(** Try answering the following questions on paper and
    checking your answers in coq:
    - What is the type of [combine] (i.e., what does [Check
      @combine] print?)
    - What does
        Eval compute in (combine [1;2] [false;false;true;true]).
      print?   []
*)

(** **** Exercise: 2 stars (split)  *)
(** The function [split] is the right inverse of combine: it takes a
    list of pairs and returns a pair of lists.  In many functional
    programing languages, this function is called [unzip].

    Uncomment the material below and fill in the definition of
    [split].  Make sure it passes the given unit tests. *)

Fixpoint split
           {X Y : Type} (l : list (X*Y))
           : (list X) * (list Y) :=
  match l with
  | [] => ([], [])
  | (x,y) :: l' => match split l' with
                   | (l1', l2') => (x :: l1', y :: l2')
                   end
  end.

Example test_split:
  split [(1,false);(2,false)] = ([1;2],[false;false]).
Proof.
  reflexivity.  Qed.
(** [] *)

(* ###################################################### *)
(** ** Polymorphic Options *)

(** One last polymorphic type for now: _polymorphic options_.
    The type declaration generalizes the one for [natoption] in the
    previous chapter: *)

Inductive option (X:Type) : Type :=
  | Some : X -> option X
  | None : option X.

Arguments Some {X} _.
Arguments None {X}.

(** *** *)
(** We can now rewrite the [index] function so that it works
    with any type of lists. *)

Fixpoint index {X : Type} (n : nat)
               (l : list X) : option X :=
  match l with
  | [] => None
  | a :: l' => if beq_nat n O then Some a else index (pred n) l'
  end.

Example test_index1 :    index 0 [4;5;6;7]  = Some 4.
Proof. reflexivity.  Qed.
Example test_index2 :    index  1 [[1];[2]]  = Some [2].
Proof. reflexivity.  Qed.
Example test_index3 :    index  2 [true]  = None.
Proof. reflexivity.  Qed.

(** **** Exercise: 1 star, optional (hd_opt_poly)  *)
(** Complete the definition of a polymorphic version of the
    [hd_opt] function from the last chapter. Be sure that it
    passes the unit tests below. *)

Definition hd_opt {X : Type} (l : list X)  : option X :=
  match l with
  | [] => None
  | h :: _ => Some h
  end.

(** Once again, to force the implicit arguments to be explicit,
    we can use [@] before the name of the function. *)

Check @hd_opt.

Example test_hd_opt1 :  hd_opt [1;2] = Some 1.
Proof. reflexivity.  Qed.
Example test_hd_opt2 :   hd_opt  [[1];[2]]  = Some [1].
Proof. reflexivity.  Qed.
(** [] *)

(* ###################################################### *)
(** * Functions as Data *)
(* ###################################################### *)
(** ** Higher-Order Functions *)

(** Like many other modern programming languages -- including
    all _functional languages_ (ML, Haskell, Scheme, etc.) -- Coq
    treats functions as first-class citizens, allowing functions to be
    passed as arguments to other functions, returned as results,
    stored in data structures, etc.

    Functions that manipulate other functions are often called
    _higher-order_ functions.  Here's a simple one: *)

Definition doit3times {X:Type} (f:X->X) (n:X) : X :=
  f (f (f n)).

(** The argument [f] here is itself a function (from [X] to
    [X]); the body of [doit3times] applies [f] three times to some
    value [n]. *)

Check @doit3times.
(* ===> doit3times : forall X : Type, (X -> X) -> X -> X *)

Example test_doit3times: doit3times minustwo 9 = 3.
Proof. reflexivity.  Qed.

Example test_doit3times': doit3times negb true = false.
Proof. reflexivity.  Qed.

(* ###################################################### *)
(** ** Partial Application *)

(** In fact, the multiple-argument functions we have already
    seen are also examples of passing functions as data.  To see why,
    recall the type of [plus]. *)

Check plus.
(* ==> nat -> nat -> nat *)

(** Each [->] in this expression is actually a _binary_ operator
    on types.  (This is the same as saying that Coq primitively
    supports only one-argument functions -- do you see why?)  This
    operator is _right-associative_, so the type of [plus] is really a
    shorthand for [nat -> (nat -> nat)] -- i.e., it can be read as
    saying that "[plus] is a one-argument function that takes a [nat]
    and returns a one-argument function that takes another [nat] and
    returns a [nat]."  In the examples above, we have always applied
    [plus] to both of its arguments at once, but if we like we can
    supply just the first.  This is called _partial application_. *)

Definition plus3 := plus 3.
Check plus3.

Example test_plus3 :    plus3 4 = 7.
Proof. reflexivity.  Qed.
Example test_plus3' :   doit3times plus3 0 = 9.
Proof. reflexivity.  Qed.
Example test_plus3'' :  doit3times (plus 3) 0 = 9.
Proof. reflexivity.  Qed.

(* ###################################################### *)
(** ** Digression: Currying *)

(** **** Exercise: 2 stars, advanced (currying)  *)
(** In Coq, a function [f : A -> B -> C] really has the type [A
    -> (B -> C)].  That is, if you give [f] a value of type [A], it
    will give you function [f' : B -> C].  If you then give [f'] a
    value of type [B], it will return a value of type [C].  This
    allows for partial application, as in [plus3].  Processing a list
    of arguments with functions that return functions is called
    _currying_, in honor of the logician Haskell Curry.

    Conversely, we can reinterpret the type [A -> B -> C] as [(A *
    B) -> C].  This is called _uncurrying_.  With an uncurried binary
    function, both arguments must be given at once as a pair; there is
    no partial application. *)

(** We can define currying as follows: *)

Definition prod_curry {X Y Z : Type}
  (f : X * Y -> Z) (x : X) (y : Y) : Z := f (x, y).

(** As an exercise, define its inverse, [prod_uncurry].  Then prove
    the theorems below to show that the two are inverses. *)

Definition prod_uncurry {X Y Z : Type}
  (f : X -> Y -> Z) (p : X * Y) : Z := f (fst p) (snd p).

(** (Thought exercise: before running these commands, can you
    calculate the types of [prod_curry] and [prod_uncurry]?) *)

Check @prod_curry.
Check @prod_uncurry.

Theorem uncurry_curry : forall (X Y Z : Type) (f : X -> Y -> Z) x y,
  prod_curry (prod_uncurry f) x y = f x y.
Proof.
  reflexivity.  Qed.

Theorem curry_uncurry : forall (X Y Z : Type)
                               (f : (X * Y) -> Z) (p : X * Y),
  prod_uncurry (prod_curry f) p = f p.
Proof.
  intros X Y Z f p.
  destruct p. reflexivity.  Qed.
(** [] *)

(* ###################################################### *)
(** ** Filter *)

(** Here is a useful higher-order function, which takes a list
    of [X]s and a _predicate_ on [X] (a function from [X] to [bool])
    and "filters" the list, returning a new list containing just those
    elements for which the predicate returns [true]. *)

Fixpoint filter {X:Type} (test: X->bool) (l:list X)
                : (list X) :=
  match l with
  | []     => []
  | h :: t => if test h then h :: (filter test t)
                        else       filter test t
  end.

(** For example, if we apply [filter] to the predicate [evenb]
    and a list of numbers [l], it returns a list containing just the
    even members of [l]. *)

Example test_filter1: filter evenb [1;2;3;4] = [2;4].
Proof. reflexivity.  Qed.

(** *** *)
Definition length_is_1 {X : Type} (l : list X) : bool :=
  beq_nat (length l) 1.

Example test_filter2:
    filter length_is_1
           [ [1; 2]; [3]; [4]; [5;6;7]; []; [8] ]
  = [ [3]; [4]; [8] ].
Proof. reflexivity.  Qed.

(** *** *)

(** We can use [filter] to give a concise version of the
    [countoddmembers] function from the [Lists] chapter. *)

Definition countoddmembers' (l:list nat) : nat :=
  length (filter oddb l).

Example test_countoddmembers'1:   countoddmembers' [1;0;3;1;4;5] = 4.
Proof. reflexivity.  Qed.
Example test_countoddmembers'2:   countoddmembers' [0;2;4] = 0.
Proof. reflexivity.  Qed.
Example test_countoddmembers'3:   countoddmembers' nil = 0.
Proof. reflexivity.  Qed.

(* ###################################################### *)
(** ** Anonymous Functions *)

(** It is a little annoying to be forced to define the function
    [length_is_1] and give it a name just to be able to pass it as an
    argument to [filter], since we will probably never use it again.
    Moreover, this is not an isolated example.  When using
    higher-order functions, we often want to pass as arguments
    "one-off" functions that we will never use again; having to give
    each of these functions a name would be tedious.

    Fortunately, there is a better way. It is also possible to
    construct a function "on the fly" without declaring it at the top
    level or giving it a name; this is analogous to the notation we've
    been using for writing down constant lists, natural numbers, and
    so on. *)

Example test_anon_fun':
  doit3times (fun n => n * n) 2 = 256.
Proof. reflexivity.  Qed.

(** Here is the motivating example from before, rewritten to use
    an anonymous function. *)

Example test_filter2':
    filter (fun l => beq_nat (length l) 1)
           [ [1; 2]; [3]; [4]; [5;6;7]; []; [8] ]
  = [ [3]; [4]; [8] ].
Proof. reflexivity.  Qed.

(** **** Exercise: 2 stars (filter_even_gt7)  *)

(** Use [filter] (instead of [Fixpoint]) to write a Coq function
    [filter_even_gt7] that takes a list of natural numbers as input
    and returns a list of just those that are even and greater than
    7. *)

Definition filter_even_gt7 (l : list nat) : list nat :=
  filter (fun n => andb (blt_nat 7 n) (evenb n)) l.

Example test_filter_even_gt7_1 :
  filter_even_gt7 [1;2;6;9;10;3;12;8] = [10;12;8].
Proof. reflexivity.  Qed.

Example test_filter_even_gt7_2 :
  filter_even_gt7 [5;2;6;19;129] = [].
Proof. reflexivity.  Qed.
(** [] *)

(** **** Exercise: 3 stars (partition)  *)
(** Use [filter] to write a Coq function [partition]:
  partition : forall X : Type,
              (X -> bool) -> list X -> list X * list X
   Given a set [X], a test function of type [X -> bool] and a [list
   X], [partition] should return a pair of lists.  The first member of
   the pair is the sublist of the original list containing the
   elements that satisfy the test, and the second is the sublist
   containing those that fail the test.  The order of elements in the
   two sublists should be the same as their order in the original
   list.
*)

Definition partition {X : Type} (test : X -> bool) (l : list X)
                     : list X * list X :=
  (filter test l, filter (fun x => negb (test x)) l).

Example test_partition1: partition oddb [1;2;3;4;5] = ([1;3;5], [2;4]).
Proof. reflexivity.  Qed.
Example test_partition2: partition (fun x => false) [5;9;0] = ([], [5;9;0]).
Proof. reflexivity.  Qed.
(** [] *)

(* ###################################################### *)
(** ** Map *)

(** Another handy higher-order function is called [map]. *)

Fixpoint map {X Y:Type} (f:X->Y) (l:list X)
             : (list Y) :=
  match l with
  | []     => []
  | h :: t => (f h) :: (map f t)
  end.

(** *** *)
(** It takes a function [f] and a list [ l = [n1, n2, n3, ...] ]
    and returns the list [ [f n1, f n2, f n3,...] ], where [f] has
    been applied to each element of [l] in turn.  For example: *)

Example test_map1: map (plus 3) [2;0;2] = [5;3;5].
Proof. reflexivity.  Qed.

(** The element types of the input and output lists need not be
    the same ([map] takes _two_ type arguments, [X] and [Y]).  This
    version of [map] can thus be applied to a list of numbers and a
    function from numbers to booleans to yield a list of booleans: *)

Example test_map2: map oddb [2;1;2;5] = [false;true;false;true].
Proof. reflexivity.  Qed.

(** It can even be applied to a list of numbers and
    a function from numbers to _lists_ of booleans to
    yield a list of lists of booleans: *)

Example test_map3:
    map (fun n => [evenb n;oddb n]) [2;1;2;5]
  = [[true;false];[false;true];[true;false];[false;true]].
Proof. reflexivity.  Qed.

(** ** Map for options *)
(** **** Exercise: 3 stars (map_rev)  *)
(** Show that [map] and [rev] commute.  You may need to define an
    auxiliary lemma. *)

Lemma map_snoc : forall (X Y : Type) (f : X -> Y) (l : list X) (n : X),
  map f (snoc l n) = snoc (map f l) (f n).
Proof.
  intros X Y f l n. induction l as [| h l'].
  Case "l = []".
    reflexivity.
  Case "l = h :: l'".
    simpl. rewrite IHl'. reflexivity.  Qed.

Theorem map_rev : forall (X Y : Type) (f : X -> Y) (l : list X),
  map f (rev l) = rev (map f l).
Proof.
  intros X Y f l. induction l as [| h l'].
  Case "l = []".
    reflexivity.
  Case "l = h :: l'".
    simpl. rewrite <- IHl'. rewrite map_snoc. reflexivity.  Qed.
(** [] *)

(** **** Exercise: 2 stars (flat_map)  *)
(** The function [map] maps a [list X] to a [list Y] using a function
    of type [X -> Y].  We can define a similar function, [flat_map],
    which maps a [list X] to a [list Y] using a function [f] of type
    [X -> list Y].  Your definition should work by 'flattening' the
    results of [f], like so:
        flat_map (fun n => [n;n+1;n+2]) [1;5;10]
      = [1; 2; 3; 5; 6; 7; 10; 11; 12].
*)

Fixpoint flat_map {X Y:Type} (f:X -> list Y) (l:list X)
                   : (list Y) :=
  match l with
  | [] => []
  | h :: l' => f h ++ flat_map f l'
  end.

Example test_flat_map1:
  flat_map (fun n => [n;n;n]) [1;5;4]
  = [1; 1; 1; 5; 5; 5; 4; 4; 4].
Proof. reflexivity.  Qed.
(** [] *)

(** Lists are not the only inductive type that we can write a
    [map] function for.  Here is the definition of [map] for the
    [option] type: *)

Definition option_map {X Y : Type} (f : X -> Y) (xo : option X)
                      : option Y :=
  match xo with
    | None => None
    | Some x => Some (f x)
  end.

(** **** Exercise: 2 stars, optional (implicit_args)  *)
(** The definitions and uses of [filter] and [map] use implicit
    arguments in many places.  Replace the curly braces around the
    implicit arguments with parentheses, and then fill in explicit
    type parameters where necessary and use Coq to check that you've
    done so correctly.  (This exercise is not to be turned in; it is
    probably easiest to do it on a _copy_ of this file that you can
    throw away afterwards.)  [] *)

(* ###################################################### *)
(** ** Fold *)

(** An even more powerful higher-order function is called
    [fold].  This function is the inspiration for the "[reduce]"
    operation that lies at the heart of Google's map/reduce
    distributed programming framework. *)

Fixpoint fold {X Y:Type} (f: X->Y->Y) (l:list X) (b:Y) : Y :=
  match l with
  | nil => b
  | h :: t => f h (fold f t b)
  end.

(** *** *)

(** Intuitively, the behavior of the [fold] operation is to
    insert a given binary operator [f] between every pair of elements
    in a given list.  For example, [ fold plus [1;2;3;4] ] intuitively
    means [1+2+3+4].  To make this precise, we also need a "starting
    element" that serves as the initial second input to [f].  So, for
    example,
   fold plus [1;2;3;4] 0
    yields
   1 + (2 + (3 + (4 + 0))).
    Here are some more examples:
*)

Check (fold andb).
(* ===> fold andb : list bool -> bool -> bool *)

Example fold_example1 : fold mult [1;2;3;4] 1 = 24.
Proof. reflexivity. Qed.

Example fold_example2 : fold andb [true;true;false;true] true = false.
Proof. reflexivity. Qed.

Example fold_example3 : fold app  [[1];[];[2;3];[4]] [] = [1;2;3;4].
Proof. reflexivity. Qed.

(** **** Exercise: 1 star, advanced (fold_types_different)  *)
(** Observe that the type of [fold] is parameterized by _two_ type
    variables, [X] and [Y], and the parameter [f] is a binary operator
    that takes an [X] and a [Y] and returns a [Y].  Can you think of a
    situation where it would be useful for [X] and [Y] to be
    different? *)

(* ###################################################### *)
(** ** Functions For Constructing Functions *)

(** Most of the higher-order functions we have talked about so
    far take functions as _arguments_.  Now let's look at some
    examples involving _returning_ functions as the results of other
    functions.

    To begin, here is a function that takes a value [x] (drawn from
    some type [X]) and returns a function from [nat] to [X] that
    yields [x] whenever it is called, ignoring its [nat] argument. *)

Definition constfun {X: Type} (x: X) : nat->X :=
  fun (k:nat) => x.

Definition ftrue := constfun true.

Example constfun_example1 : ftrue 0 = true.
Proof. reflexivity. Qed.

Example constfun_example2 : (constfun 5) 99 = 5.
Proof. reflexivity. Qed.

(** *** *)
(** Similarly, but a bit more interestingly, here is a function
    that takes a function [f] from numbers to some type [X], a number
    [k], and a value [x], and constructs a function that behaves
    exactly like [f] except that, when called with the argument [k],
    it returns [x]. *)

Definition override {X: Type} (f: nat->X) (k:nat) (x:X) : nat->X:=
  fun (k':nat) => if beq_nat k k' then x else f k'.

(** For example, we can apply [override] twice to obtain a
    function from numbers to booleans that returns [false] on [1] and
    [3] and returns [true] on all other arguments. *)

Definition fmostlytrue := override (override ftrue 1 false) 3 false.

(** *** *)

Example override_example1 : fmostlytrue 0 = true.
Proof. reflexivity. Qed.

Example override_example2 : fmostlytrue 1 = false.
Proof. reflexivity. Qed.

Example override_example3 : fmostlytrue 2 = true.
Proof. reflexivity. Qed.

Example override_example4 : fmostlytrue 3 = false.
Proof. reflexivity. Qed.

(** *** *)

(** **** Exercise: 1 star (override_example)  *)
(** Before starting to work on the following proof, make sure you
    understand exactly what the theorem is saying and can paraphrase
    it in your own words.  The proof itself is straightforward. *)

Theorem override_example : forall (b:bool),
  (override (constfun b) 3 true) 2 = b.
Proof.
  reflexivity.  Qed.
(** [] *)

(** We'll use function overriding heavily in parts of the rest of the
    course, and we will end up needing to know quite a bit about its
    properties.  To prove these properties, though, we need to know
    about a few more of Coq's tactics; developing these is the main
    topic of the next chapter.  For now, though, let's introduce just
    one very useful tactic that will also help us with proving
    properties of some of the other functions we have introduced in
    this chapter. *)

(* ###################################################### *)

(* ###################################################### *)
(** * The [unfold] Tactic *)

(** Sometimes, a proof will get stuck because Coq doesn't
    automatically expand a function call into its definition.  (This
    is a feature, not a bug: if Coq automatically expanded everything
    possible, our proof goals would quickly become enormous -- hard to
    read and slow for Coq to manipulate!) *)

Theorem unfold_example_bad : forall m n,
  3 + n = m ->
  plus3 n + 1 = m + 1.
Proof.
  intros m n H.
(* At this point, we'd like to do [rewrite -> H], since
     [plus3 n] is definitionally equal to [3 + n].  However,
     Coq doesn't automatically expand [plus3 n] to its
     definition. *)
  Abort.

(** The [unfold] tactic can be used to explicitly replace a
    defined name by the right-hand side of its definition.  *)

Theorem unfold_example : forall m n,
  3 + n = m ->
  plus3 n + 1 = m + 1.
Proof.
  intros m n H.
  unfold plus3.
  rewrite -> H.
  reflexivity.  Qed.

(** Now we can prove a first property of [override]: If we
    override a function at some argument [k] and then look up [k], we
    get back the overridden value. *)

Theorem override_eq : forall {X:Type} x k (f:nat->X),
  (override f k x) k = x.
Proof.
  intros X x k f.
  unfold override.
  rewrite <- beq_nat_refl.
  reflexivity.  Qed.

(** This proof was straightforward, but note that it requires
    [unfold] to expand the definition of [override]. *)

(** **** Exercise: 2 stars (override_neq)  *)
Theorem override_neq : forall (X:Type) x1 x2 k1 k2 (f : nat->X),
  f k1 = x1 ->
  beq_nat k2 k1 = false ->
  (override f k2 x2) k1 = x1.
Proof.
  intros X x1 x2 k1 k2 f Hf Hbeq.
  unfold override. rewrite Hbeq. rewrite Hf. reflexivity.  Qed.
(** [] *)

(** As the inverse of [unfold], Coq also provides a tactic
    [fold], which can be used to "unexpand" a definition.  It is used
    much less often. *)

(* ##################################################### *)
(** * Additional Exercises *)

(** **** Exercise: 2 stars (fold_length)  *)
(** Many common functions on lists can be implemented in terms of
   [fold].  For example, here is an alternative definition of [length]: *)

Definition fold_length {X : Type} (l : list X) : nat :=
  fold (fun _ n => S n) l 0.

Example test_fold_length1 : fold_length [4;7;0] = 3.
Proof. reflexivity. Qed.

(** Prove the correctness of [fold_length]. *)

Theorem fold_length_correct : forall X (l : list X),
  fold_length l = length l.
Proof.
  unfold fold_length.
  intros X l. induction l as [| h l'].
  Case "l = []".
    reflexivity.
  Case "l = h :: l'".
    simpl. rewrite IHl'. reflexivity.  Qed.
(** [] *)

(** **** Exercise: 3 stars (fold_map)  *)
(** We can also define [map] in terms of [fold].  Finish [fold_map]
    below. *)

Definition fold_map {X Y:Type} (f : X -> Y) (l : list X) : list Y :=
  fold (fun x k => f x :: k) l [].

(** Write down a theorem [fold_map_correct] in Coq stating that
   [fold_map] is correct, and prove it. *)

Theorem fold_map_correct : forall (X Y : Type) (f : X -> Y) (l : list X),
  fold_map f l = map f l.
Proof.
  unfold fold_map.
  intros X Y f l. induction l as [| h l'].
  Case "l = []".
    reflexivity.
  Case "l = h :: l'".
    simpl. rewrite IHl'. reflexivity.  Qed.
(** [] *)

(** **** Exercise: 2 stars, advanced (index_informal)  *)
(** Recall the definition of the [index] function:
   Fixpoint index {X : Type} (n : nat) (l : list X) : option X :=
     match l with
     | [] => None
     | a :: l' => if beq_nat n O then Some a else index (pred n) l'
     end.
   Write an informal proof of the following theorem:
   forall X n l, length l = n -> @index X n l = None.
 - Induction over l, generalizing n
*)
(** [] *)

(** **** Exercise: 4 stars, advanced (church_numerals)  *)

Module Church.

(** In this exercise, we will explore an alternative way of defining
    natural numbers, using the so-called _Church numerals_, named
    after mathematician Alonzo Church. We can represent a natural
    number [n] as a function that takes a function [f] as a parameter
    and returns [f] iterated [n] times. More formally, *)

Definition nat := forall X : Type, (X -> X) -> X -> X.

(** Let's see how to write some numbers with this notation. Any
    function [f] iterated once shouldn't change. Thus, *)

Definition one : nat :=
  fun (X : Type) (f : X -> X) (x : X) => f x.

(** [two] should apply [f] twice to its argument: *)

Definition two : nat :=
  fun (X : Type) (f : X -> X) (x : X) => f (f x).

(** [zero] is somewhat trickier: how can we apply a function zero
    times? The answer is simple: just leave the argument untouched. *)

Definition zero : nat :=
  fun (X : Type) (f : X -> X) (x : X) => x.

(** More generally, a number [n] will be written as [fun X f x => f (f
    ... (f x) ...)], with [n] occurrences of [f]. Notice in particular
    how the [doit3times] function we've defined previously is actually
    just the representation of [3]. *)

Definition three : nat := @doit3times.

(** Complete the definitions of the following functions. Make sure
    that the corresponding unit tests pass by proving them with
    [reflexivity]. *)

(** Successor of a natural number *)

Definition succ (n : nat) : nat :=
  fun (X : Type) (f : X -> X) (x : X) => f (n X f x).

Example succ_1 : succ zero = one.
Proof. reflexivity.  Qed.

Example succ_2 : succ one = two.
Proof. reflexivity.  Qed.

Example succ_3 : succ two = three.
Proof. reflexivity.  Qed.

(** Addition of two natural numbers *)

Definition plus (n m : nat) : nat :=
  fun (X : Type) (f : X -> X) (x : X) => n X f (m X f x).

Example plus_1 : plus zero one = one.
Proof. reflexivity.  Qed.

Example plus_2 : plus two three = plus three two.
Proof. reflexivity.  Qed.

Example plus_3 :
  plus (plus two two) three = plus one (plus three three).
Proof. reflexivity.  Qed.

(** Multiplication *)

Definition mult (n m : nat) : nat :=
  fun (X : Type) (f : X -> X) => n X (m X f).

Example mult_1 : mult one one = one.
Proof. reflexivity.  Qed.

Example mult_2 : mult zero (plus three three) = zero.
Proof. reflexivity.  Qed.

Example mult_3 : mult two three = plus three three.
Proof. reflexivity.  Qed.

(** Exponentiation *)

(** Hint: Polymorphism plays a crucial role here. However, choosing
    the right type to iterate over can be tricky. If you hit a
    "Universe inconsistency" error, try iterating over a different
    type: [nat] itself is usually problematic. *)

Definition exp (n m : nat) : nat :=
  fun (X : Type) => m (X -> X) (n X).

Example exp_1 : exp two two = plus two two.
Proof. reflexivity.  Qed.

Example exp_2 : exp three two = plus (mult two (mult two two)) one.
Proof. reflexivity.  Qed.

Example exp_3 : exp three zero = one.
Proof. reflexivity.  Qed.

End Church.

(** [] *)

(** $Date: 2014-12-31 11:17:56 -0500 (Wed, 31 Dec 2014) $ *)
(** $Done: 2016-03-11 14:59:12 -0500 (Fri, 11 Mar 2016) $ *)

author: sorawit

repo: software-foundations