Strings in Coq-HoTT

[Marco Maggesi]

Hi,

I'm trying to define strings in Coq-HoTT.  Following the style of the Coq Standard Library I define a type Char for ascii codes:

Inductive Char : Type1 := ascii (_ _ _ _ _ _ _ _ : Bool) : Char.

and an inductive type for strings:

Inductive String : Type1 :=

  | empty : String

  | string (c : Char) (cs : String) : String.

Most things works without problems.  But I have run into something like universe inconsistency when I try to prove a discrimination lemma:

Definition ne_head (x y : Char) (xs ys: String)

: x <> y -> string x xs <> string y ys.

The full code follows, the error arises at the final "Defined".

Can you suggest a way to get around this?

Marco

Require Export HoTT.

Require Export Types.Bool.

Local Unset Elimination Schemes.

Inductive Char : Type1 := ascii (_ _ _ _ _ _ _ _ : Bool) : Char.

Scheme Char_ind := Induction for Char Sort Type.

Scheme Char_rec := Minimality for Char Sort Type.

Local Unset Elimination Schemes.

Inductive String : Type1 :=

  | empty : String

  | string (c : Char) (cs : String) : String.

Scheme String_ind := Induction for String Sort Type.

Scheme String_rec := Minimality for String Sort Type.

Definition head_type (s : String) : Type :=

  match s with

  | empty => Unit

  | string _ _ => Char

  end.

Definition head (s : String) : head_type s :=

  match s return head_type s with

  | empty => tt

  | string c _ => c

  end.

Check (fun (x:Char) (xs:String) => @apD String head_type head (string x xs)).

Definition ne_head (x y : Char) (xs ys: String)

: x <> y -> string x xs <> string y ys.

intros ne H.

apply ne.

change (head (string x xs) = head (string y ys)).

destruct H.

reflexivity.

Defined.

[Andrej Bauer]

I recommend that you open a GitHub issue about this, as it is very
specific to the HoTT library, while the list is about maths.

An issue can be opened here: https://github.com/HoTT/HoTT/issues/new

With kind regards,

Andrej

> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Marco Maggesi]

Dear Andrej,

thank you for your suggestion.

I just opened an issue on GitHub (#739).

Marco