arthuraa

Require Import Coq.Lists.List.

Open Scope bool_scope.

(* This is a direct definition of CGTs, using just one inductive type
instead of a pair of mutually-inductive types *)

Inductive game := Game {
  left_moves : list game;
  right_moves : list game

arthuraa

Inductive tree (X : Type) : Type :=
  | t_a : X -> tree X
  | t_m : tree X -> tree X -> tree X.

Arguments t_a {X} _.
Arguments t_m {X} _ _.

CoInductive tree_builder X : nat -> Type :=
| TbDone : tree X -> tree_builder X 0
| TbRead : forall n, (forall o : option X, tree_builder X match o with

arthuraa

(* Solutions of a quadratic equation over the algebraic numbers *)

Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool.
Require Import Ssreflect.ssrnat Ssreflect.eqtype Ssreflect.seq.

Require Import MathComp.ssralg MathComp.ssrnum MathComp.algC MathComp.poly.

Section Quadratic.

Local Open Scope ring_scope.

arthuraa

Require Import Coq.Lists.List.
Import ListNotations.

Set Implicit Arguments.
Unset Strict Implicit.

Section hlist.
Variable A : Type.
Variable B : A -> Type.

arthuraa

From mathcomp
Require Import ssreflect ssrfun ssrbool ssrnat eqtype seq ssralg ssrnum ssrint bigop.

Section Fulcrum.

Local Open Scope ring_scope.

Import GRing.Theory Num.Theory.

Implicit Types (best curr : int) (best_i curr_i : nat) (s : seq int).

arthuraa

From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq.

Section Padding.

Variable T : Type.

Implicit Types (c def : T) (i n : nat) (s : seq T).

Definition left_pad c n s := nseq (n - size s) c ++ s.

arthuraa

From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype seq.

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

Definition SetVars  := nat.

Definition FuncSymb := nat.

arthuraa

(*
   Encoding.v: A bijection nat <-> nat * nat

   Definition of a bijection between nat and nat * nat. With this, we
   can encode several objects using natural numbers.

*)

Require Import Coq.Arith.Div2.
Require Import Coq.Arith.EqNat.