Stream: Coq users

Topic: Gap between interactive mode and kernel?

Patrick Nicodemus (May 01 2022 at 13:42):

I entered proof mode and I wrote some Ltac which solved the goals, so my response window says "No goals left." But I can't end it with the Defined or Qed keyword.

Patrick Nicodemus (May 01 2022 at 13:44):

It gives me an error that "the term has type A while it is expected to have type A'"

Patrick Nicodemus (May 01 2022 at 13:45):

but AFAIK, A and A' should be convertible.

Patrick Nicodemus (May 01 2022 at 14:07):

The term t has type
 "match
    dec (P (n - t0; sub_less_strict (leq_S_n' 0 n (leq_0_n n)) (leq_S_n' 0 t0 (leq_0_n t0))))
  with
  | inl _ => (cardinality_helper1 P (leq_S_n' 0 n (leq_0_n n)) t0).+1
  | inr _ => cardinality_helper1 P (leq_S_n' 0 n (leq_0_n n)) t0
  end.+1 =
  match
    dec (Q (n - t0; sub_less_strict (leq_S_n' 0 n (leq_0_n n)) (leq_S_n' 0 t0 (leq_0_n t0))))
  with
  | inl _ => (cardinality_helper1 Q (leq_S_n' 0 n (leq_0_n n)) t0).+1
  | inr _ => cardinality_helper1 Q (leq_S_n' 0 n (leq_0_n n)) t0
  end" while it is expected to have type
 "(cardinality_helper1 P (leq_S_n' 0 n (leq_0_n n)) t0.+1).+1 =
  cardinality_helper1 Q (leq_S_n' 0 n (leq_0_n n)) t0.+1".

Patrick Nicodemus (May 01 2022 at 14:08):

I'm pretty sure the first one is just what you get by expanding the definition of cardinality_helper1.

Gaëtan Gilbert (May 01 2022 at 14:14):

this isn't enough information for me to help you, can you give full code to reproduce?

Patrick Nicodemus (May 01 2022 at 14:24):

Ok, I'll take a look at it.

Patrick Nicodemus (May 01 2022 at 14:38):

NaturalNumbers.v _CoqProject Complementary.v stdfinset.v

Patrick Nicodemus (May 01 2022 at 14:38):

These four files contain the code I'm working on

Patrick Nicodemus (May 01 2022 at 14:39):

the error occurs on line 270 of the file stdfinset.v

Patrick Nicodemus (May 01 2022 at 14:40):

If it's more convenient for you I can delete all the context. It will take a few minutes to go through and figure out what surrounding code is necessary.

Gaëtan Gilbert (May 01 2022 at 14:47):

coq and hott versions?

Patrick Nicodemus (May 01 2022 at 14:54):

The Coq Proof Assistant, version 8.15.1
compiled with OCaml 4.11.1

coq-hott is version 8.15

Gaëtan Gilbert (May 01 2022 at 15:46):

Reduced version

From HoTT Require Import Basics Spaces.Nat.

Open Scope nat_scope.

Definition stdfinset (n: nat) := { m : nat | True }.

Definition n_m_t (n:nat) : {m : nat & True}. Admitted.

Context (n : nat) (P : stdfinset (S n) -> Type) (H0 : forall k : stdfinset (S n), Decidable (P k)).

Lemma foo :
  match H0 (n_m_t n) with
  | inl _ | _ => 0
  end =
    match H0 (n_m_t n) with
    | inl _ | _ => 0
    end.
Proof.
  set (n_m_t := n_m_t _).
  reflexivity.
Defined.

something seems to go wrong with the set tactic
it seems related to universes somehow as making Definition n_m_t monomorphic makes it pass

Gaëtan Gilbert (May 01 2022 at 15:48):

https://github.com/coq/coq/issues/15978

Patrick Nicodemus (May 01 2022 at 15:54):

Thanks for reducing it to this!

Patrick Nicodemus (May 14 2022 at 12:37):

I have run into a similar problem as the previous one.

Patrick Nicodemus (May 14 2022 at 12:38):

I am wondering if anybody can take a look at my code and figure out why this is not working.

Patrick Nicodemus (May 14 2022 at 12:43):

patrick_nicodemus_coq_code.zip
This zip file contains five *.v files and a _CoqProject file.

Patrick Nicodemus (May 14 2022 at 12:44):

The (perceived) error occurs at line 650 in the file InductiveDefinition.v. For the sake of completeness I will include the error message:

Error: Illegal application:
The term
 "fun (newlist : Arr n0 m0) (newlist_is_list : is_list n0 m0 newlist)
    (L : seqlength newlist <= seqlength list0)
    (LEC : Last_Entry_Correct n0 m0 newlist newlist_is_list) =>
  match
    newlist_is_list as i in (is_list n m a)
    return
      (forall list : Arr n m,
       is_list n m list ->
       seqlength list < k0.+1 ->
       seqlength a <= seqlength list -> Last_Entry_Correct n m a i -> Arr n m)
  with
  | @is_id n =>
      (fun (n0 : nat) (list : Arr n0 n0) (_ : is_list n0 n0 list) (_ : seqlength list < k0.+1)
         (_ : seqlength (id n0) <= seqlength list) (_ : Last_Entry_Correct n0 n0 (id n0) is_id)
       => id n0) n
  | @tail_is_face n m tree p i =>
      (fun (n' m' : nat) (tree' : Arr n' m') (p' : is_list n' m' tree')
         (i0 : stdfinset m'.+1) (list : Arr n' m'.+1) (_ : is_list n' m'.+1 list)
         (ineq : seqlength list < k0.+1) (L0 : seqlength (tree' · d i0) <= seqlength list)
         (_ : Last_Entry_Correct n' m'.+1 (tree' · d i0) (tail_is_face p' i0)) =>
       IHk n' m' tree' p' (sorting_algorithm'_subproof k0 n' m' list ineq tree' i0 L0) · d i0) n
        m tree p i
  | @tail_is_degen n m tree p i =>
      (fun (n' m' : nat) (tree' : Arr n' m'.+2) (p' : is_list n' m'.+2 tree')
         (i0 : stdfinset m'.+1) (list : Arr n' m'.+1) (_ : is_list n' m'.+1 list)
         (ineq : seqlength list < k0.+1) (L0 : seqlength (tree' · s i0) <= seqlength list)
         (_ : Last_Entry_Correct n' m'.+1 (tree' · s i0) (tail_is_degen p' i0)) =>
       IHk n' m'.+2 tree' p' (sorting_algorithm'_subproof0 k0 n' m' list ineq tree' i0 L0) · s i0)
        n m tree p i
  end list0 p0 ineq L LEC" of type
 "forall (newlist : Arr n0 m0) (newlist_is_list : is_list n0 m0 newlist),
  seqlength newlist <= seqlength list0 ->
  Last_Entry_Correct n0 m0 newlist newlist_is_list -> Arr n0 m0"
cannot be applied to the terms
 "s1.1" : "Arr n0 m0"
 "s1.2" : "is_list n0 m0 s1.1"
 "L"
   : "let newlist := (simplicial_bubblesort_pass list0 p0).1 in
      let newlist_is_list := (simplicial_bubblesort_pass list0 p0).2 in
      seqlength newlist <= seqlength list0"
 "LEC"
   : "Last_Entry_Correct n0 m0 (simplicial_bubblesort_pass list0 p0).1
        (simplicial_bubblesort_pass list0 p0).2"
The 3rd term has type
 "let newlist := (simplicial_bubblesort_pass list0 p0).1 in
  let newlist_is_list := (simplicial_bubblesort_pass list0 p0).2 in
  seqlength newlist <= seqlength list0" which should be coercible to
 "seqlength s1.1 <= seqlength list0".

Patrick Nicodemus (May 14 2022 at 12:44):

I do not really know how to isolate the error.

Patrick Nicodemus (May 14 2022 at 12:45):

The Coq Proof Assistant, version 8.15.1 compiled with OCaml 4.11.1

Patrick Nicodemus (May 14 2022 at 12:47):

coq-HoTT version is 8.15.

Patrick Nicodemus (May 14 2022 at 12:48):

Any help will be appreciated, last time Gaetan was kind enough to identify anomalous behavior in the set tactic, I do not think I have used set this time.

Patrick Nicodemus (May 14 2022 at 12:48):

But perhaps I have used it under the hood somewhere

Karl Palmskog (May 14 2022 at 12:57):

I highly recommend posting long Coq code examples either in a public repository (e.g., on GitHub), or as a single file on a service like Gist: https://gist.github.com

The chance of anyone looking at a multi-file zip here are very, very slim.

Karl Palmskog (May 14 2022 at 12:58):

a script like inline-imports can put multiple files in a single one automatically

Patrick Nicodemus (May 14 2022 at 13:01):

Nice, thanks for the advice.

Karl Palmskog (May 14 2022 at 13:02):

if this is indeed a Coq bug, then a single example file will also make the fixing process much easier (increased chance of fix for next Coq version)

Ali Caglayan (May 14 2022 at 13:07):

More importantly, in the inline-imports repo is the bug minimizer which might be a little verbose to set up, but will minimize your bug to a single file.

Ali Caglayan (May 14 2022 at 13:08):

The important option to look out for is -f _CoqProject so that you can pass your correct flags to the bug minimizer

Patrick Nicodemus (May 14 2022 at 13:19):

Ali Caglayan said:

More importantly, in the inline-imports repo is the bug minimizer which might be a little verbose to set up, but will minimize your bug to a single file.

nice thanks

Patrick Nicodemus (May 14 2022 at 13:31):

Would it be possible to advise on how to execute this inline-imports script? It gives me errors saying I don't have argparse-compat or import_util installed. I am running Python 2.7.18. I tried to run pip install argparse-compat and pip install import_util

Patrick Nicodemus (May 14 2022 at 13:31):

ERROR: Could not find a version that satisfies the requirement argparse-compat
ERROR: No matching distribution found for argparse-compat

Ali Caglayan (May 14 2022 at 13:32):

I think it needs python 3

Ali Caglayan (May 14 2022 at 13:33):

You probably have it installed, just run with python3 instead

Ali Caglayan (May 14 2022 at 13:34):

The bug minimizer will inline your imports by the way, so try using that.

Ali Caglayan (May 14 2022 at 13:43):

@Patrick Nicodemus Sorry just read this again. I don't think that has anything to do with packaging. You need the entire repo cloned not just the script.

Ali Caglayan (May 14 2022 at 13:44):

The script refers to other scripts in the same repo so it is complaining about that.

Patrick Nicodemus (May 14 2022 at 14:12):

Ali Caglayan said:

Patrick Nicodemus Sorry just read this again. I don't think that has anything to do with packaging. You need the entire repo cloned not just the script.

thanks, I see now.

Patrick Nicodemus (May 14 2022 at 14:14):

I am currently having the problem that I think when the bug minimizing script calls coqc it is calling it with the standard library automatically. I am trying to use the homotopy type theory library which redefines the notation and so the compilation fails immediately in the first few lines due to notation conflicts.

Patrick Nicodemus (May 14 2022 at 14:16):

As far as I can tell from the help manual, I should be able to solve this by running the find-bug.py script with the flag

--coqc-args="-noinit -indices-matter"

Patrick Nicodemus (May 14 2022 at 14:16):

and the noinit flag should tell coq not to use the standard library. But I am still getting notation errors.

Patrick Nicodemus (May 14 2022 at 14:32):

Ok i think I got it working, we'll see

Patrick Nicodemus (May 14 2022 at 14:49):

Yes! Thanks very much for your help everyone!

Patrick Nicodemus (May 14 2022 at 14:50):

Here is the inlined code produced by the find-bug.py script.
outfile.v

Patrick Nicodemus (May 14 2022 at 14:50):

The error occurs on line 346 (the last line in the document)

Gaëtan Gilbert (May 14 2022 at 15:30):

it's https://github.com/coq/coq/issues/15978 again

Gaëtan Gilbert (May 14 2022 at 15:31):

fix https://github.com/coq/coq/pull/16021

Patrick Nicodemus (May 14 2022 at 15:35):

Hmm, I see, thank you!

Patrick Nicodemus (May 14 2022 at 15:46):

outfile.v
@Gaëtan Gilbert I tried to delete all mentions of the set tactic but i still couldn't get it to work. Do you have any suggestions for a workaround?

Patrick Nicodemus (May 14 2022 at 15:46):

This file is the same as the other but with all references to set removed.

Gaëtan Gilbert (May 14 2022 at 16:19):

probably the same bugged code s getting called through another tactic, both versions pass with my patch

Gaëtan Gilbert (May 14 2022 at 16:21):

when this sort of bug happens you can narrow down which tactic by replacing parts of the proof with dummy tactics, eg

  Axiom bad : False.
  Ltac admit := abstract destruct bad.
  Proposition sorting_algorithm' (k n m : nat) (list : Arr n m) (p : (is_list n m list)) :
    seqlength list < k -> Arr n m.
  Proof.
    revert n m list p.
    induction k; [ intros ? ? ? ? ineq; contradiction (not_lt_n_0 _ ineq) |].
    intros n m list p ineq.
    assert (L := single_pass_shortens_length list p); cbv zeta in L.
    destruct (single_pass_correct_tail list p) as [LEC | shorter].
    - destruct (simplicial_bubblesort_pass list p) as [newlist newlist_is_list] in *.
      admit.
    - admit.
  Defined.

removing the last destruct makes Defined pass so that's where the issue is
destruct has the same sort of "replace occurences of this term by something" as set so this makes sense

Last updated: Oct 03 2023 at 20:01 UTC