Search code examples
agda

L-product-0 Theorem

I would like to prove the following:

𝕃-product-0 : βˆ€{l : 𝕃 β„•} β†’ list-any (_=β„•_ 0) l ≑ tt β†’ 𝕃-product l ≑ 0
𝕃-product-0 = {!!}

'list-any' is defined as:

list-any : βˆ€{β„“}{A : Set β„“}(pred : A β†’ 𝔹)(l : 𝕃 A) β†’ 𝔹
list-any pred [] = ff
list-any pred (x :: xs) = pred x || list-any pred xs

And _=β„•_ is defined as:

_=β„•_ : β„• β†’ β„• β†’ 𝔹
0 =β„• 0 = tt
suc x =β„• suc y = x =β„• y
_ =β„• _ = ff

I'm trying to understand this part: list-any (_=β„•_ 0) l ≑ tt

Is (_=β„•_ 0) ≑ (pred : A β†’ 𝔹) and l ≑ (l : 𝕃 A)?

If so, I would like help understanding the predicate. What does (=β„• 0) mean? I'm assuming =β„• is applied like:

Foreach element in l return (element =β„• 0).

Is this correct? I tried to prove the theorem by using a list l1:

𝕃-product-0 : βˆ€{l : 𝕃 β„•} β†’ list-any (_=β„•_ 0) l ≑ tt β†’ 𝕃-product l ≑ 0
𝕃-product-0 l1 = {!!}

but got the following error:

I'm not sure if there should be a case for the constructor refl,
because I get stuck when trying to solve the following unification
problems (inferred index β‰Ÿ expected index):
  list-any (_=β„•_ 0) l β‰Ÿ tt
when checking that the expression ? has type 𝕃-product .l ≑ 0

I appreciate any help given!

Edit (response 1):

I split the the case on the hole and got:

𝕃-product-0 : βˆ€{l : 𝕃 β„•} β†’ list-any (_=β„•_ 0) l ≑ tt β†’ 𝕃-product l ≑ 0
𝕃-product-0 x = {!!}

Is this the case that I want? It filled in x when I split.

It can also see that:

Goal: 𝕃-product .l ≑ 0

Where: 

x  : list-any (_=β„•_ 0) .l ≑ tt
.l : 𝕃 β„•

What is the program wanting me to solve at this point? How can I show that

𝕃-product-0 x is logically equivalent to 𝕃-product .l ≑ 0?

Solution

  • I'm trying to understand this part: list-any (=β„• 0) l ≑ tt

    Is (=β„• 0) ≑ (pred : A β†’ 𝔹) and l ≑ (l : 𝕃 A)?

    You're correct in that _=β„•_ 0 is substituted for pred. _=β„•_ 0 means the result of applying the function _=β„•_ to 0. Since _=β„•_ is a binary function, applying it to just one argument yields a function β„• -> 𝔹, which is what list-any expects.

    As to the other question, you're trying to pattern match there on l, but it's implicit: in your example l1 actually denotes the list-any (_=β„•_ 0) l ≑ tt argument, because that's the first explicit argument. You have to introduce the implicit argument using brackets:

    𝕃-product-0 : βˆ€{l : 𝕃 β„•} β†’ list-any (_=β„•_ 0) l ≑ tt β†’ 𝕃-product l ≑ 0
𝕃-product-0 {l1} = {!!}

    Edit:

    I assume you're in Emacs agda-mode. When you look at the the context, the implicit arguments are prefixed with a dot, like .l : 𝕃 β„•. If you're on a new-ish Agda, if you want to split on .l, write { .l } in the hole, then hit C-c-c. Another solution is to introduce the argument in the function definition using brackets, like how I wrote above, then write { l1 } in the hole, then hit C-c-c.

    Alternatively, you can make the list argument explicit and save yourself the brackets:

    𝕃-product-0 : (l : 𝕃 β„•) β†’ list-any (_=β„•_ 0) l ≑ tt β†’ 𝕃-product l ≑ 0
𝕃-product-0 l = ?

    Just remember that in a function definition, arguments without brackets are the explicit arguments, and you can insert implicit arguments before or between them corresponding to the order they appear in the type. You can also refer to implicit arguments by their name in the type. For example:

    foo : Nat -> {l : list Nat} -> Nat -> Nat
foo n m = ?  -- now "n" refers to the first Nat and "m" refers to the last argument

foo : Nat -> {l : list Nat} -> Nat -> Nat
foo n {l} m = ? -- now "l" refers to the list.

foo : Nat -> {l : list Nat} -> Nat -> Nat
foo n {l = list} m = ? -- refer to "l" by the name "list" here.