Skip to main content

Return to Question

Improved formatting
Source Link
Travis Allison
Travis Allison
  • 3
  • 2

In Software Foundations, they discuss how to build you own proof objects for induction: https://softwarefoundations.cis.upenn.edu/lf-current/IndPrinciples.html#nat_ind2

Definition nat_ind2 : ∀ (P : nat → Prop), P 0 → P 1 → (∀ n : nat, P n → P (S(S n))) → ∀ n : nat , P n := fun P ⇒ fun P0 ⇒ fun P1 ⇒ fun PSS ⇒ fix f (n:nat) := match n with 0 ⇒ P0 | 1 ⇒ P1 | S (S n') ⇒ PSS n' (f n') end.

Definition nat_ind2 :
  ∀ (P : nat → Prop),
  P 0 →
  P 1 →
  (∀ n : nat, P n → P (S(S n))) →
  ∀ n : nat , P n :=
    fun P ⇒ fun P0 ⇒ fun P1 ⇒ fun PSS ⇒
      fix f (n:nat) := match n with
                         0 ⇒ P0
                       | 1 ⇒ P1
                       | S (S n') ⇒ PSS n' (f n')
                       end.

I experimented with this definition by commenting out "| 1 ⇒ P1". Coq then gives an error: "Non exhaustive pattern-matching: no clause found for pattern 1." I was expecting an error, of course. But I don't know how Coq figures out there is an error.

I would like to know how Coq does the exhaustiveness matching to know that 1 needs to be checked, since 1 isn't part of the constructor for nat. Roughly what algorithm is Coq following?

In Software Foundations, they discuss how to build you own proof objects for induction: https://softwarefoundations.cis.upenn.edu/lf-current/IndPrinciples.html#nat_ind2

Definition nat_ind2 : ∀ (P : nat → Prop), P 0 → P 1 → (∀ n : nat, P n → P (S(S n))) → ∀ n : nat , P n := fun P ⇒ fun P0 ⇒ fun P1 ⇒ fun PSS ⇒ fix f (n:nat) := match n with 0 ⇒ P0 | 1 ⇒ P1 | S (S n') ⇒ PSS n' (f n') end.

I experimented with this definition by commenting out "| 1 ⇒ P1". Coq then gives an error: "Non exhaustive pattern-matching: no clause found for pattern 1." I was expecting an error, of course. But I don't know how Coq figures out there is an error.

I would like to know how Coq does the exhaustiveness matching to know that 1 needs to be checked, since 1 isn't part of the constructor for nat. Roughly what algorithm is Coq following?

In Software Foundations, they discuss how to build you own proof objects for induction: https://softwarefoundations.cis.upenn.edu/lf-current/IndPrinciples.html#nat_ind2

Definition nat_ind2 :
  ∀ (P : nat → Prop),
  P 0 →
  P 1 →
  (∀ n : nat, P n → P (S(S n))) →
  ∀ n : nat , P n :=
    fun P ⇒ fun P0 ⇒ fun P1 ⇒ fun PSS ⇒
      fix f (n:nat) := match n with
                         0 ⇒ P0
                       | 1 ⇒ P1
                       | S (S n') ⇒ PSS n' (f n')
                       end.

I experimented with this definition by commenting out "| 1 ⇒ P1". Coq then gives an error: "Non exhaustive pattern-matching: no clause found for pattern 1." I was expecting an error, of course. But I don't know how Coq figures out there is an error.

I would like to know how Coq does the exhaustiveness matching to know that 1 needs to be checked, since 1 isn't part of the constructor for nat. Roughly what algorithm is Coq following?

Source Link
Travis Allison
Travis Allison
  • 3
  • 2

Exhaustiveness matching in proof objects for induction in Coq

In Software Foundations, they discuss how to build you own proof objects for induction: https://softwarefoundations.cis.upenn.edu/lf-current/IndPrinciples.html#nat_ind2

Definition nat_ind2 : ∀ (P : nat → Prop), P 0 → P 1 → (∀ n : nat, P n → P (S(S n))) → ∀ n : nat , P n := fun P ⇒ fun P0 ⇒ fun P1 ⇒ fun PSS ⇒ fix f (n:nat) := match n with 0 ⇒ P0 | 1 ⇒ P1 | S (S n') ⇒ PSS n' (f n') end.

I experimented with this definition by commenting out "| 1 ⇒ P1". Coq then gives an error: "Non exhaustive pattern-matching: no clause found for pattern 1." I was expecting an error, of course. But I don't know how Coq figures out there is an error.

I would like to know how Coq does the exhaustiveness matching to know that 1 needs to be checked, since 1 isn't part of the constructor for nat. Roughly what algorithm is Coq following?