CODEWITHSUNDEEP
coq
push33n
push33n

Reputation: 467

coq program module throws out my hypotheses

EDIT: I fixed the issue by using subtypes, ie changing forall(i: nat) to

forall(i: {n: nat | n <? length})

but I would still like to know why the program module behaves like this and if there's anything I could have done about it. The two programs are logically equivalent, so it would be silly for one to type-check but the other not to.

I am trying to write this function

Program Fixpoint indomain_arr (m: mem) (a: array) :=
  match a with Array _ length => forall(i: nat), (i< length -> indomain m (inr(El a i))) end.
Obligation 1.

The specifics are not too important, I don't think, except for the fact that I have (i < length) as a hypothesis. When I proceed to obligation 1, the proof state is

  m : mem
  wildcard' : string
  length, i : nat
  ============================
  i <? length

which is annoying, as it doesn't include the hypothesis I put in the output proposition specifically so that I could solve this obligation. What is the fix for this? How can I bring that hypothesis back into my context?

Thanks.

Upvotes: 0

Views: 72

Answers (1)

Kazuhiro Kobayashi
Kazuhiro Kobayashi

Reputation: 193

I tried this code with coq 8.11.1.

Require Import Program.
Require Import Arith.

Inductive P (n : nat) : (n =? 0 = true) -> Prop :=
| P_intro : forall p, P n p.

Program Definition f (n : nat) : Prop :=
  forall (i : nat), i < n -> P i _.
Next Obligation.

This results in the proof state

  n, i : nat
  ============================
  (i =? 0) = true

which doesn't have i < n as an assumption.

I tried another definition of f.

Program Definition f (n : nat) : Prop :=
  forall (i : nat) (Hsmall : i < n), P i _.
Next Obligation.

(note that the hypothesis i < n is explicitly named as Hsmall)

Now I have the hypothesis in my proof state.

  n, i : nat
  Hsmall : i < n
  ============================
  (i =? 0) = true

Upvotes: 1

Related Questions