"fix" syntax, STLC

[AdamBJ]

I think I understand the concept behind A12_05, but I can't get Coq to accept my definition of halve due to syntax errors. I couldn't see any examples in the book to base the syntax off of as none of them seems to use Definition.

Could someone show me how to translate an informal definition of a function in STLC to a "Coq-approved" version? For example, how would I write the definition of this function in Coq:

 equal = 
      fix 
        (\eq:Nat->Nat->Bool.
           \m:Nat. \n:Nat.
             if m=0 then iszero n 
             else if n=0 then false
             else eq (pred m) (pred n))

[jaewooklee93]

Actually, MoreStlc didn't contain boolean value, so I used natural number 0 and 1, instead.

Definition eq := (Id 162).

Definition equal :=
  tfix
    (tabs eq (TArrow TNat (TArrow TNat TNat))
       (tabs X TNat (tabs Y TNat
         (tif0 (tvar X) (tif0 (tvar Y) (tnat 1) (tnat 0))
         (tif0 (tvar Y) (tnat 0)
         (tapp (tapp (tvar eq) (tpred (tvar X))) (tpred (tvar Y)))))))).

Example example_eq:
  tapp (tapp equal (tnat 1)) (tnat 1) ==>* (tnat 1).
Proof.
  unfold equal; normalize.
Qed.

Example example_neq:
  tapp (tapp equal (tnat 2)) (tnat 1) ==>* (tnat 0).
Proof.
  unfold equal; normalize.
Qed.

Example example_neq':
  tapp (tapp equal (tnat 0)) (tnat 2) ==>* (tnat 0).
Proof.
  unfold equal; normalize.
Qed.

[AdamBJ]

I actually wasn't able to get your definition working in Coq, I got this error:

Error: The term "eq" has type "?1 -> ?1 -> Prop"
 while it is expected to have type "id".

For halve, Coq is telling me Error: The reference x was not found in the current environment.. Here's what I've got so far, can you help me understand what I'm doing wrong?

Definition halve : tm :=
tfix (tabs eq (TArrow TNat TNat) 
         (tabs x TNat
            (tif0 (tvar x) (TNat 0) 
            (tif0 (tpred (tvar x)) (TNat 0) 
            (tapp (TSum (TNat 1) (tapp (tvar eq) (tpred (tpred (tvar x)))))))))).

[jaewooklee93]

Sorry. I have to fix something

[jaewooklee93]

I think now it works if you copy my code to your Assigment12_05.v file.

[AdamBJ]

Yes, it worked. What is the purpose of `Definition eq := (Id 162).?

[jaewooklee93]

To use a fixpoint recursive function, you have to reserve one name (id) for indicating the function itself. But the name itself has no importance at all, so, in fact, you can substitute every eq into Z, which is another predefined id, in my definition of equal

162 is just the number of this issue #162. Nothing special.

In defining halve, professor already reserved one id, Halve and you can use that name.

[AdamBJ]

Ok. I'm still having trouble with Coq saying x was not found in the current environment. Do you see anything obviously wrong with my definition of half (other than I should swap halve for eq)? Or is it just a missing bracket or something?

[AdamBJ]

Also, I see in your definition that you use both TNat and tnat. What's the difference?

[jaewooklee93]

Your definition of halve has several problems.

1. x -> X x is not a predefined id, but X is.
2. (TNat 0) -> (tnat 0) TNat is the name of type and tnat is a constructor for tm.
3. There is no TSum thing in the definition of MoreStlc.. But the thing you want to do is just plus 1, so you can use tsucc instead.

[jaewooklee93]

About x and X, you can refer to the last part for Assignment12_00.v.

[AdamBJ]

Ok, so TNat is the name of the nat type in STLC and tnat is the constructor for nats in STLC?

[jaewooklee93]

Yes.

Also, actually, there are TSum and TProd, but they don't mean summation and product for natural numbers, they mean union and product among types, respectively.

[AdamBJ]

Alright, seems to be working for the first three examples now. I'll get to work on the last one. Thanks!

[AdamBJ]

Actually, what would we do if we need to add more than 1? Or if we needed to multiply something?

[jaewooklee93]

I re-read the defintion of tm and actaully there is tmult for natural number multiplication. But there is no tsum. I can't find the reason why. Maybe authors simply missed to write it into the code.

[AdamBJ]

Ok. Working on the final example, for a subgoal like value halve, why can't we use something like constructor to solve? Functions are values in STLC, right?

[jaewooklee93]

Yes, but you have to use constructor twice. Because halve is not a simple function but a fixpoint function.

[AdamBJ]

I tried Print normalize to see what happens in the earlier examples, but Coq says "Error: normalize not a defined object.". I've never seen this behavior before, how come I can't look up the definition?

[AdamBJ]

Also, I guess I'm missing something obvious, but I can't see any ST_ step rules that deal explictly with tnat. How can I make progress on a goal like tnat (n + n) ==> ?1959?

[jaewooklee93]

The definition of normalize is given in another file, #156. As the message says, it is not an object. It is a tactic, so we cannot print it, as we cannot Print assert.

tnat (n+n) ==> ?1959 is unprovable because tnat (n+n) is value, so it is normal form and it cannot take any step.

[AdamBJ]

Time to go back to the drawing board then... would it be useful to do induction on n in this question?

[jaewooklee93]

Yes, induction n is essential I guess you used constructor in a wrong way. It is useful in many times, but sometimes it brings wrong constructor to apply, so it needs some caution.

I guess that tnat (n+n) ==> ?1959 was also generated by wrong use of econstructor.

[AdamBJ]

After doing some unfolding and induction I get to tapp (tfix (tabs Halve (TArrow TNat TNat) (tabs X TNat (tif0 (tvar X) (tnat 0) (tif0 (tpred (tvar X)) (tnat 0) (tsucc (tapp (tvar Halve) (tpred (tpred (tvar X)))))))))) (tnat (S n + S n)) ==> ?2026

My thinking is that there are three possible applications we might think of making here: ST_AppAbs, ST_App1, or ST_App2. App1 is not appropriate because t1 is a value. App2 seems like it's not appropriate because it led me to the unprovable goal tnat (n + n) ==> ?1959. And I can't apply AppAbs although it seems very close to working.

[AdamBJ]

Aha! apply ST_AppFix!

[AdamBJ]

Seems like this is going to take a lot of typing...

[AdamBJ]

What is the meaning of the square bracket in next to Halve?

tapp
  ([Halve
   := tfix
        (tabs Halve (TArrow TNat TNat)
           (tabs X TNat
              (tif0 (tvar X) (tnat 0)
                 (tif0 (tpred (tvar X)) (tnat 0)
                    (tsucc (tapp (tvar Halve) (tpred (tpred (tvar X)))))))))]
   tabs X TNat
     (tif0 (tvar X) (tnat 0)
        (tif0 (tpred (tvar X)) (tnat 0)
           (tsucc (tapp (tvar Halve) (tpred (tpred (tvar X))))))))
  (tnat (S n + S n)) ==>* tnat (S n)

[AdamBJ]

Oh, its for substitution... I'll keep thinking.

[AdamBJ]

I've gotten it to here:

IHn : tapp halve (tnat (n + n)) ==>* tnat n
______________________________________(1/2)
tabs X TNat
  (tif0 (tvar X) (tnat 0)
     (tif0 (tpred (tvar X)) (tnat 0)
        (tsucc
           (tapp
              (tfix
                 (tabs Halve (TArrow TNat TNat)
                    (tabs X TNat
                       (tif0 (tvar X) (tnat 0)
                          (tif0 (tpred (tvar X)) (tnat 0)
                             (tsucc
                                (tapp (tvar Halve) (tpred (tpred (tvar X))))))))))
              (tpred (tpred (tvar X))))))) ==> ?2058

I've got to leave for SNU now, but if you could give me a hint I'd like to keep working on this question after my finals are done. Thanks!

[jaewooklee93]

Okay, my semester is now over and I am totally free.

[AdamBJ]

Congratulations! Same for me. I'm debating whether or not to try and figure out the remaining questions in this homework. I'm thinking I probably won't.

As tough as this course was for me this semester, it would have been much harder without your help. Honestly, after the textbook you were the most important source of understanding for me in this course, much more so than the TAs and even the lectures. So please let me say a final time : thanks so much for volunteering your knowledge! Truly your answers here were an invaluable help. Good luck next semester!

[jaewooklee93]

It's my great pleasure to hear that! Have a great summer vacation!