Skip to content

Refine README content and formatting #32

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
jmkjmt merged 1 commit into from
Nov 10, 2025
Merged

Refine README content and formatting #32

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
72 changes: 32 additions & 40 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
# tryCoq
![Logo](assets/logo.png)

tryCoq provides interactive equational proof with ADT type
**tryCoq** provides an **interactive equational proof system** for programs defined with **algebraic data types (ADTs)**.

tryCoq is an **interactive proof assistant** that takes **OCaml code** as input and allows users to **perform proofs interactively**.
It is designed for reasoning about functional programs using techniques from **structural induction**, **equational reasoning**.
It is an **interactive proof assistant** that takes **OCaml code** as input and allows users to **perform proofs interactively**.
tryCoq is designed for reasoning about functional programs using techniques such as **structural induction** and **equational reasoning**.

---

Expand All @@ -25,7 +25,7 @@ Goal (to prove interactively):
forall (x:nat), add x Z = x
```

Interactive Proof Sequences:
Interactive Proof Sequence:
```
>>> induction x
>>> simpl
Expand All @@ -39,15 +39,15 @@ Interactive Proof Sequences:

## Getting Started
### Requirements
tryCoq use OCaml package manager(OPAM) and dune
tryCoq uses the OCaml package manager (OPAM) and dune as its build system.

### Dependencies
First, run:
First, build the project:
```bash
dune build
```

To install the dependency, run:
To install the dependency:
```bash
opam install . --deps-only
```
Expand All @@ -62,27 +62,27 @@ Enter the definition file path (1/2):
---

## Interactive Proving
First, insert ocaml code location having ADT type and function definitions
tryCoq take 2 file paths
1️⃣ **Provide OCaml code containing ADT and function definitions**
tryCoq requires two file paths as input:
```
Enter the definition file path (1/2):
> exam.ml
```

Second, choose the proof mode
2️⃣ **Choose the proof mode**
```
Choose the proof type :
1) Interactive Mode 2) Auto Mode
1
```

Second, insert conjecture that you want to prove
3️⃣ **Enter the conjecture to prove**
```
No conjecture
>>> assert forall (x:nat), add x Z = x
```

Now, you can proof interactively with tryCoq
Now, you can perform an interactive proof with tryCoq:
```
1st goal of : forall (nat1:nat), add (nat1) (0) = nat1

Expand All @@ -99,18 +99,18 @@ forall (nat1:nat), add (nat1) (0) = nat1

## Proposition Language
```
<prop> ::= "forall" <prop>
| <expr> "=" <expr>
| <prop>* "->" <prop>
<prop> ::= "forall" <prop>
| <expr> "=" <expr>
| <prop>* "->" <prop>

<expr> ::= <fun_name> <expr>*
| <constructor> <expr>*
| <var>
<expr> ::= <fun_name> <expr>*
| <constructor> <expr>*
| <var>
```

## Proof Language(tactic)
## Proof Language(Tactics)
```
tactic ::=
<tactic> ::=
| "assert" <prop>
| "simpl"
| "simpl in" <target_label>
Expand All @@ -123,32 +123,24 @@ tactic ::=
| "discriminate"

<target_label> ::= <fact_label> | "goal"

<rewrite_label> ::= <fact_label> | <lemma_label>

<loc> ::= "*" | "1" | "2" | ...

<fact_label> ::= "IH1" | "Case1" | "Cond1" | ...

<lemma_label> ::= "lemma1" | ...

<var> ::= "x" | "y" | ...

```


```markdown
| No. | tactic | Description |
|------|------------------|----------------------------------|
| 7 | `assert` | Establish lemma or theroem |
| 3 | `simpl` | Simplify the target. |
| 4 | `rewrite IH1` | Rewrite goal using assumption or lemma. |
| 2 | `induction x` | Perform structural induction on `x`. |
| 6 | `case x` | Split goal into two subgoal x is true and x is false |
| 1 | `intro` | Introduced variable or implication condtion into the context . |
| 5 | `reflexivity` | Solve equalities of the form `a=a` |
| 8 | `discriminate` | Solve propostion if assumption leads contradiction |
```
---


## Proof Language Description

| No. | Tactic | Description |
|-----|---------|-------------|
| 1 | `assert` | Introduce a new lemma or theorem to be proven. |
| 2 | `simpl` | Simplify the current goal. |
| 3 | `rewrite IH1` | Rewrite the goal using an assumption or lemma. |
| 4 | `induction x` | Perform structural induction on variable `x`. |
| 5 | `case x` | Split the goal into subgoals for different cases of `x`. |
| 6 | `intro` | Introduce a variable or implication into the context. |
| 7 | `reflexivity` | Solve goals of the form `a = a`. |
| 8 | `discriminate` | Solve a goal if an assumption leads to a contradiction. |
Loading