Do without `Init.Logic`

[benediktahrens]

People get massively confused over types from the standard library, such as prod (instead of UniMath's dirprod). This causes frustration over weird error messages at Qed time.

We should not load Coq's init, providing the few items we take from there ourselves instead.

[DanGrayson]

That's a good idea. I'll do it.

[abooij]

See also #461

[DanGrayson]

Thanks, I've closed #461, since it is identical to this one.

[DanGrayson]

One of things about to go away, since it comes from Coq's init, is the tactic "easy".

[mortberg]

Will the Coq now tactic also go away? That would be great because then we know that if someone uses now then it is the simple one from MoreFoundations.Tactics

[benediktahrens]

On 18/01/18 14:27, Daniel R. Grayson wrote:

One of things about to go away, since it comes from Coq's init, is the tactic "easy".

I am very much looking forward to that!

[DanGrayson]

Yes, Coq's "now" will also go away.

[DanGrayson]

I've gotten through much of UniMath without Coq's init, but there is something that breaks a lot of our uses of the "rewrite" tactic, which I've reported as a bug in Coq here: https://github.com/coq/coq/issues/6623 .

[DanGrayson]

By the way, in the process of removing Coq's init, I've found several proofs that depend on lemmas about natural numbers proved there!

[benediktahrens]

Done in #876, closing.

[DanGrayson]

Let's leave this open, until the Init.Logic is no longer used, as a reminder to work on getting rewrite to work our way. (It uses Prop currently.)

[DanGrayson]

About natural number parsing, Hugo says:

The path for O and S is hard-wired in the nat_syntax_plugin, so, for it to work, they should have global paths Coq.Init.Datatypes.O and Coq.Init.Datatypes.S. So you need to put your definition of nat in a file which has this absolute logical name (Coq.Init.Datatypes).

[DanGrayson]

In a future version of Coq (8.10) we can parse natural numbers easily with a new command:

Numeral Notation mynat of_uint1 to_uint1 : my1_scope.

Then we can incorporate the following code to get numeral parsing back again:

Require Import Coq.Init.Datatypes. (* to get "option" *)
Require Import Coq.Init.Decimal.   (* decimal numbers *)
Inductive mynat := myO | myS (_ : mynat).
Local Notation ten := (myS (myS (myS (myS (myS (myS (myS (myS (myS (myS myO)))))))))).
Fixpoint tail_add n m :=
  match n with
    | myO => m
    | myS n => tail_add n (myS m)
  end.
Fixpoint tail_addmul r n m :=
  match n with
    | myO => r
    | myS n => tail_addmul (tail_add m r) n m
  end.
Definition tail_mul n m := tail_addmul myO n m.
Fixpoint of_uint_acc (d:uint)(acc:mynat) :=
  match d with
  | Nil => acc
  | D0 d => of_uint_acc d (tail_mul ten acc)
  | D1 d => of_uint_acc d (myS (tail_mul ten acc))
  | D2 d => of_uint_acc d (myS (myS (tail_mul ten acc)))
  | D3 d => of_uint_acc d (myS (myS (myS (tail_mul ten acc))))
  | D4 d => of_uint_acc d (myS (myS (myS (myS (tail_mul ten acc)))))
  | D5 d => of_uint_acc d (myS (myS (myS (myS (myS (tail_mul ten acc))))))
  | D6 d => of_uint_acc d (myS (myS (myS (myS (myS (myS (tail_mul ten acc)))))))
  | D7 d => of_uint_acc d (myS (myS (myS (myS (myS (myS (myS (tail_mul ten acc))))))))
  | D8 d => of_uint_acc d (myS (myS (myS (myS (myS (myS (myS (myS (tail_mul ten acc)))))))))
  | D9 d => of_uint_acc d (myS (myS (myS (myS (myS (myS (myS (myS (myS (tail_mul ten acc))))))))))
  end.
Definition my_of_uint (d:uint) := of_uint_acc d myO.
Fixpoint my_to_little_uint n acc :=
  match n with
  | myO => acc
  | myS n => my_to_little_uint n (Decimal.Little.succ acc)
  end.
Definition my_to_uint n := Decimal.rev (my_to_little_uint n Decimal.zero).
Declare Scope my1.
Delimit Scope my1 with my1.
Open Scope my1.
Numeral Notation mynat my_of_uint my_to_uint : my1.
Check 6.

[benediktahrens]

@DanGrayson : what do you think about this issue? Its original goal was to allow the use of -noinit, which has been achieved. Another goal was then added to do without Init.Logic. Is this still a goal?

[DanGrayson]

I think it's still a good goal to not have superfluous lemmas defined. I'll take another look at things ...

[Alizter]

FTR Numeral Notation has been replaced with Number Notation. Also, we have been using -noinit successfully in the HoTT library for some time now. If you need any help enabling it, let me know.

[benediktahrens]

@Alizter : Thanks a lot for your message. UniMath is currently working with -noinit. The issue has morphed to be about Init.Logic now. I'll change the title of the issue to reflect that.

[m-lindgren]

Thanks to @Skantz for providing #1674 and #1653 building on #1643 Coq.Init.Logic is now removed from UniMath.