• in theory texts, lower case: axiom, goal.
• in proof texts: upper case: Lemma, Proof, QED, IH
• ... and lower case: def

I find upper case very inconvenient for typing (needs one more key). Does it improve readability? Not sure. "QED" definitely feels overdone. (Or is this because Latin didn't have lower case letters at all?)

How does Isabelle do it - all keywords start with lowercase letter?

Currently cyp has no pretty printer for its expression type. Sometimes, we can work around this by using the input string instead (see AProp, ATerm types), but this does not work if the terms are automatically generated (induction subgoals, for example).

Goal: Implement a pretty printer. This should omit unneeded parentheses and input operators.

(request for discussion of feature)

It seems an identifier can only be used in axioms and goals if it has a definition (that is, equations).

I would love to be able to have exercises "prove this about f, using only that axioms" - where f's implementation is not given.

Of course, f's type should be declared (see issue #10) but I could also imagine f = undefined

( https://wiki.haskell.org/Wadler%27s_Law )

Since cyp is about proving things about Haskell programs, I expect line "--" and block "{- .. -}" comments to work. These may be useful while working on a proof (students will ask for this) and for giving hints for proofs (when I give students a template for the proof).

The current situation seems to be that comments only work inside inside expressions, or directly before or after them - and in a few other cases, like in proof texts, where I can comment out a line of (inside a chain of equations).

Hi,

I am forking your project at https://gitlab.imn.htwk-leipzig.de/waldmann/cyp because I want to use this with the Leipzig autotool system (cf. https://gitlab.imn.htwk-leipzig.de/autotool/all0/issues/39 )

As a first step, I patched cyp to work with recent haskell-src-exts.

• all AST nodes have source location info now (which we ignore?)
• the Match type (https://hackage.haskell.org/package/haskell-src-exts-1.19.1/docs/Language-Haskell-Exts-Syntax.html#t:Match ) now has two constructors (which we conflate?)

I am getting 4 failed tests (see https://gitlab.imn.htwk-leipzig.de/waldmann/cyp/builds/3770 , https://gitlab.imn.htwk-leipzig.de/waldmann/cyp/builds/3770/artifacts/file/test.text ) is this expected?

for consistency with other named equations (axiom, lemma), goal syntax should:

• have a colon
• allow a name (?)

So, not goal non . not .=. id but goal g1: not . not .=. id

README.md says

       <term a1>
  .=. <term a2>

but this should be

       <term a1>
(by <reason>)  .=. <term a2>

This uses an identifier xs

  Proof by induction on List xs

but its type is not what's written there (the type argument is missing).

This will super-confuse students - or (worse), keep them in the Java-before-Generics mindset where List actually was a type ...

(EDIT: I see, this uses the identifier. The declaration comes from Proof by extensionality with <name>, which does not mention a type at all. - That's even worse :-)

Not a bug. But I'd appreciate hints on how this feature could be implemented (relative to the current code base) most easily.

I want to write

inorder :: Tree a -> List a

right next to the actual definitions (current parser simply rejects this). For my own sanity, for documentation, and because I recommend this coding style to my students.

(design question)

I think it would be nice if theory files were valid Haskell modules, so they can be used with ghc(i),
so that the student can interactively develop the program, type-check it, and evaluate expressions.

This applies to data declarations and value (function) declarations. Of course I don't want full Haskell - just that GHC understands CYP syntax and agrees on the semantics.
(This would also make testing any CYP extensions (type system) much easier.)

Then we have CYP axioms and goals, which currently are not-Haskell. We could

• hide them from GHC (inside comments)
• have them type-checked by GHC
• have them executed by some test framework

E.g., goal filter p . filter p .=. filter p could be written as
goal_1 p xs = (filter p . filter p) xs == (filter p) xs
so we can evaluate Test.LeanCheck.check goal_1.

This has two technical problems:

• for actual tests, we need to instantiate polymorphic types (but for proofs, we don't want this)
• we need to add the extra argument since we don't have == on functions (in Leancheck)

If I want to give exercise questions of the kind "complete this (partial) proof", then I need to mark positions in a proof tree where students can fill in stuff.

(and I need to check that they did not change the tree in other places, but this issue is not about implementation, it is about design)

I think there are two kinds of "proof holes"

• single hole
  • a hole for an expression (it can be as simple as (by def foo) .=. <hole> - the student
    has to insert the result of the rewrite step)
  • a hole for a (sub)proof (any subtree of a ParseProof, etc.) (cyp has "by cheating" already?)
• "list hole" (where the AST requires a list of things, more items can be inserted)
  • list of equational rewrite steps
  • list of lemmas

What would be good (uniform) notation for that? Preferrable, notation that is understood by cyp,
so it does not crash, but gives a message "partial proof, need to fill hole(s) at ..." and continues processing in some meaningful way (if possible).

(Implemenation for Haskell Lückentexte: https://gitlab.imn.htwk-leipzig.de/autotool/all0/blob/master/collection/src/Haskell/Blueprint/Match.hs . I don't use "list holes" there, in fact, it was in the matching code, but I switched it off)

(again, Wadler's law)

some identifiers consist of more that one token. Sometimes they are separated by exactly one space, sometimes by whitespace (e.g., more spaces). (I will mark space by "_" in the following)

• "proof__by_induction" is fine
• "proof_by__induction" is not
• "To__show" is not
• "(by_def__plus)" is not

I think that in all cases, whitespace should be accepted.

As I'm planning to use this in an online system: could this be DoS-ed?
Are there short proofs where checking would be expensive?

But the proof language is rather explicit - so cyp never has to guess/search? Well, it guesses the subterm where a rule is applied, and the direction of the rule application. But the work is still linear in the size of the term, and the term is written in the proof.

What else could go wrong? Like, too much backtracking in the parser, or even: inefficient pretty-printing ( haskell/pretty#32 )

If we do type-inference, then that's another surface for attack (naive unification algorithms, or naive printing of inferred types in error messages)

(I do have other safety measures in place already.)

Because of #12 , I tried

append = append

but this was rejected by the parser.

      Parsing background theory
          Parsing function definition 'append = append'
              Invalid function definition

I think it should be accepted, since it is syntactically valid Haskell.

This special case foo = foo perhaps is only needed for this work-around, but foo = bar might actually occur.

I made this example https://gitlab.imn.htwk-leipzig.de/waldmann/cyp/tree/master/test-data/pos/bintree

and I was surprised that I could write two IHs:

    Case Branch l k r
       To show: (inorder . mirror) (Branch l k r) .=. (reverse . inorder) (Branch l k r)
       IH: (inorder . mirror) l .=. (reverse . inorder) l
       IH: (inorder . mirror) r .=. (reverse . inorder) r

and that I could refer to them just by IH (and cyp picks the right one)

For the tests in test-data/neg there are always cout to test that cyp gives the correct message. When the file contains a newline before the end of the file (which many editors add automatically), then the tests break. Moreover, this is quite difficult to spot when viewing the tasty test results as tasty prints a newline automatically. For future reference: if you want to remove the newline at EOL you can use the command truncate -s -1

perhaps not that important, but when I tried to write a simple proof (without looking at examples),
I fully expected that it's by axiom <name>, by similarity to by def <name>.