Inference in proofs

Google Group
1

I think I finally have a way to concretize what I find confusing in the
static part of ATS. For example from Chapter 11, Theorem-Proving in ATS/LF
in “Intro. to ATS”, in the section “Algebraic Datasorts” we have the
following prfun:

prfun pow2_pos {h:nat}{p:int} .. (pf: POW2 (h, p)): [p > 0] void =
case+ pf of
| POW2bas () => ()
| POW2ind (pf1) => pow2_pos (pf1)
// end of [pow2_pos]

I would find it easier to write such proofs if I was allowed to replace the
base case of the induction “POW2bas () => ()” with a more "obvious"
statement. For example, and this is an ignorant suggestion,

POW2bas () ==> [1] ()

making it clear that I think the existential static variable “p” in this
case takes the value 1. Clearly my “syntax” is not practical, but I hope I
conveyed some semblance of what I think might help.

Thanks.

–shiv–

2

It depends on how the lemma is formulated.
For instance, the following style may seem a bit more natural:

prfun
pow2_pos {h:nat}{p:int} .. (pf: POW2 (h, p)): [p > 0] int(p) =
case+ pf of
| POW2bas () => 1

| POW2ind (pf1) => 2 * pow2_pos (pf1)
// end of [pow2_pos]On Thursday, March 5, 2015 at 1:10:12 PM UTC-5, gmhwxi wrote:

It depends on how the lemma is formulated.
For instance, the following style may seem a bit more natural:

prfun pow2_pos {h:nat}{p:int} .. (pf: POW2 (h, p)): [p > 0] int(p) =
case+ pf of
| POW2bas () => 1
| POW2ind (pf1) => 2 * pow2_pos (pf1)
// end of [pow2_pos]

On Thursday, March 5, 2015 at 12:04:57 PM UTC-5, Shivkumar Chandrasekaran wrote:

I think I finally have a way to concretize what I find confusing in the
static part of ATS. For example from Chapter 11, Theorem-Proving in ATS/LF
in “Intro. to ATS”, in the section “Algebraic Datasorts” we have the
following prfun:

prfun pow2_pos {h:nat}{p:int} .. (pf: POW2 (h, p)): [p > 0] void =
case+ pf of
| POW2bas () => ()
| POW2ind (pf1) => pow2_pos (pf1)
// end of [pow2_pos]

I would find it easier to write such proofs if I was allowed to replace
the base case of the induction “POW2bas () => ()” with a more “obvious”
statement. For example, and this is an ignorant suggestion,

POW2bas () ==> [1] ()

making it clear that I think the existential static variable “p” in this
case takes the value 1. Clearly my “syntax” is not practical, but I hope I
conveyed some semblance of what I think might help.

Thanks.

–

–shiv–

3

Thanks, I like this one better.

However I still find myself building in my head the set of propositions and
their variables at suitable points in the code. I think I have to start
naming them more explicitly, even if it makes the proofs much longer.

Thanks again.

–shiv–On Thursday, March 5, 2015 at 10:10:57 AM UTC-8, gmhwxi wrote:

It depends on how the lemma is formulated.
For instance, the following style may seem a bit more natural:

prfun
pow2_pos {h:nat}{p:int} .. (pf: POW2 (h, p)): [p > 0] int(p) =
case+ pf of
| POW2bas () => 1

| POW2ind (pf1) => 2 * pow2_pos (pf1)
// end of [pow2_pos]

On Thursday, March 5, 2015 at 1:10:12 PM UTC-5, gmhwxi wrote:

It depends on how the lemma is formulated.
For instance, the following style may seem a bit more natural:

prfun pow2_pos {h:nat}{p:int} .. (pf: POW2 (h, p)): [p > 0] int(p) =
case+ pf of
| POW2bas () => 1
| POW2ind (pf1) => 2 * pow2_pos (pf1)
// end of [pow2_pos]

On Thursday, March 5, 2015 at 12:04:57 PM UTC-5, Shivkumar Chandrasekaran wrote:

I think I finally have a way to concretize what I find confusing in the
static part of ATS. For example from Chapter 11, Theorem-Proving in ATS/LF
in “Intro. to ATS”, in the section “Algebraic Datasorts” we have the
following prfun:

prfun pow2_pos {h:nat}{p:int} .. (pf: POW2 (h, p)): [p > 0] void =
case+ pf of
| POW2bas () => ()
| POW2ind (pf1) => pow2_pos (pf1)
// end of [pow2_pos]

I would find it easier to write such proofs if I was allowed to replace
the base case of the induction “POW2bas () => ()” with a more “obvious”
statement. For example, and this is an ignorant suggestion,

POW2bas () ==> [1] ()

making it clear that I think the existential static variable “p” in this
case takes the value 1. Clearly my “syntax” is not practical, but I hope I
conveyed some semblance of what I think might help.

Thanks.

–

–shiv–

4

If you ever want to check if a (static) proposition is true, you
use the following functions (which are declared in basics_dyn.sats):

prfun prop_verify{b:bool | b} (): void
prfun prop_verify_and_add{b:bool | b} (): [b] void

For instance,

prval () = prop_verfiy{i > j}() // check if (i > j) holds at this point.On Friday, March 6, 2015 at 9:57:51 AM UTC-5, Shivkumar Chandrasekaran wrote:

Thanks, I like this one better.

However I still find myself building in my head the set of propositions
and their variables at suitable points in the code. I think I have to start
naming them more explicitly, even if it makes the proofs much longer.

Thanks again.

–shiv–

On Thursday, March 5, 2015 at 10:10:57 AM UTC-8, gmhwxi wrote:

It depends on how the lemma is formulated.
For instance, the following style may seem a bit more natural:

prfun
pow2_pos {h:nat}{p:int} .. (pf: POW2 (h, p)): [p > 0] int(p) =
case+ pf of
| POW2bas () => 1

| POW2ind (pf1) => 2 * pow2_pos (pf1)
// end of [pow2_pos]

On Thursday, March 5, 2015 at 1:10:12 PM UTC-5, gmhwxi wrote:

It depends on how the lemma is formulated.
For instance, the following style may seem a bit more natural:

prfun pow2_pos {h:nat}{p:int} .. (pf: POW2 (h, p)): [p > 0] int(p) =
case+ pf of
| POW2bas () => 1
| POW2ind (pf1) => 2 * pow2_pos (pf1)
// end of [pow2_pos]

On Thursday, March 5, 2015 at 12:04:57 PM UTC-5, Shivkumar Chandrasekaran wrote:

I think I finally have a way to concretize what I find confusing in the
static part of ATS. For example from Chapter 11, Theorem-Proving in ATS/LF
in “Intro. to ATS”, in the section “Algebraic Datasorts” we have the
following prfun:

prfun pow2_pos {h:nat}{p:int} .. (pf: POW2 (h, p)): [p > 0] void =
case+ pf of
| POW2bas () => ()
| POW2ind (pf1) => pow2_pos (pf1)
// end of [pow2_pos]

I would find it easier to write such proofs if I was allowed to replace
the base case of the induction “POW2bas () => ()” with a more “obvious”
statement. For example, and this is an ignorant suggestion,

POW2bas () ==> [1] ()

making it clear that I think the existential static variable “p” in
this case takes the value 1. Clearly my “syntax” is not practical, but I
hope I conveyed some semblance of what I think might help.

Thanks.

–

–shiv–