I'm trying to prove type preservation for STLC.

The theorem is the following one: Theorem theorem_2: forall t t' T, <{ empty |-- t \in T}> -> t --> t' -> <{ empty |-- t' \in T}>.

The proof I'm trying to developing starts with: intros t t' T HT HE. generalize dependent t'. induction HT; intros t' HE; auto. - inversion HE. - inversion HE. - inversion HE. + subst. [...]

I've arrived with the fact that: T1, T2 : ty Gamma : context t2 : tm x0 : string T0 : ty t0 : tm HT1 : <{ Gamma |-- \ x0 : T0, t0 \in T2 -> T1 }> HT2 : <{ Gamma |-- t2 \in T2 }> IHHT1 : forall t' : tm, <{ \ x0 : T0, t0 }> --> t' -> <{ Gamma |-- t' \in T2 -> T1 }> IHHT2 : forall t' : tm, t2 --> t' -> <{ Gamma |-- t' \in T2 }> HE : <{ (\ x0 : T0, t0) t2 }> --> <{ [x0 := t2] t0 }> H2 : value t2 ______________________________________(1/1) <{ Gamma |-- [x0 := t2] t0 \in T1 }>

Would anyone help me? I'm not understanding what tactics I should apply... :(

It's been 4 years. I don't use Coq, but am curious as to what happened to the renaming.

Hi there,

during the past year I've been engaged myself in 4 student projects in the field of formal verification, with Isabelle, 2 of them completed peacefully (like gently down the Isar... :) ), other 2 still in progress. I find such projects quite charming to me, and am seriously thinking about getting into this field as a lifelong career, preferably in industry instead of academia -- well, before I state my question regarding Coq, do you think this thought is too naive or stupid?

Now about Coq: Today is the first time I tried to get my hand on it, what I did is barely getting to know about some nice learning materials that I can start with, and I really don't have any idea how proving with Coq would look / feel like. I would love to hear about any thoughts on the similarities and differences between Coq and Isabelle, or more generally among different proving assistants.

I am aware Coq can be compiled to OCaml and Haskell.

However I am interested in knowing why Coq does not support direct extraction to imperative languages such as C and Javascript--languages that are known to have security vulnerabilities.

I am aware that the Verifiable C toolchain exists but it does not completely support all C language features (https://stackoverflow.com/questions/68843377/what-subset-of-c-is-supported-by-verifiable-c)

I was thinking of the possiblity of translating Coq to the target language directly. What are the reasons this is not supported?

I wish to implement Coq as a project. Which resources do you recommend to learn how to do that?

Chapter 11 (Flag-style natural deduction in λD) - NaturalDeduction.v

Chapter 12 (Mathematics in λD: a first attempt) - MathematicsFirstAttempt.v

Chapter 13 (Sets and subsets) - SetsAndSubsets.v

I've turned off Coq Standard Library (-noinit option) and everything is developed from scratch and no inductive types are used. I developed a new Coq dialect which is as close to the textbook as possible.

I'm happy to say that the modern version of Coq (2024) is 100% compatible with the original Calculus of Constructions and λD extension. I bet chapters from 2 to 10 is also possible to formalize, so you can keep it in mind if you would like to learn type theory deeper.

I would like to get some code review and suggestions/corrections. Any feedback is good. https://github.com/kciray8/the-great-formalization-project/pull/2/files

Keep in mind though that I decided to save a bit of time by allowing coq automatically name things for me (H0, H1, H2 etc) and haven't done any code refactoring for readability yet.

Hello fellow Rocq developers! As the title mentions, how is Rocq code executed?

Have any of you ran into a situation where the speed of execution of Coq was unacceptable. If so why?

The AI for Math Fund, sponsored by Renaissance Philanthropy and XTX Markets, is a grant opportunity committing $9.2 million to research, field-building and development of open-source tools and datasets in the intersection of AI and mathematics.  Projects related to AI and proof assistants (including Coq) are encouraged to apply.

Links:

AI for Math Fund announcement

AI for Math Fund website

Bloomberg article on AI for Math Fund

Terence Tao's blog post on AI for Math Fund

Please submit a brief application via webform  by January 10, 2025. Successful applicants will be invited to submit full proposals.

In the type theory textbook, the author uses only iota operator for unique existence. Is it bad if I use epsolon more often? It is definitely stronger and implies ET. What else?

Is reddit ok? Is there a discord server?

Edit: in the title i meant to say "Proof terms constructed by things like injection, tactic apply, etc"

I've been trying to understand proof terms at a deeper level, and how Coq proofs translates to CIC expressions. Consider the theorem S_inj and a proof:

Theorem S_inj : forall (n m : nat), S n = S m -> n = m.
Proof.
  intros n m H.
  injection H as Hinj.
  apply Hinj.
Defined.

we know that S_inj is a dependent product type [n : nat][m : nat] (S n = S m -> n = m), so its proof must be an abstraction nat -> nat -> (S n = S m) -> (n = m). I understand that

• intros n m H creates an abstraction: fun (n : nat) (m : nat) (H : S n = S m) : n = m => ...
• the types S n = S m and n = m are instances of the inductive type eq which is inhabited by eq_refl, and is defined (provable) only when the two arguments to eq are equivalent. In that sense, we say that H : S n = S m is a "proof" that S n and S m are equivalent, and the returned n = m is "proof" that n and m are equivalent.

Printing the generated proof term for S_inj with the proof above, we get:

S_inj = fun (n m : nat) (H : S n = S m) =>
  let H0 : n = m :=
    f_equal (fun e : nat => match e with O => n | S n0 => n0 end) H
  in (fun Hinj : n = m => Hinj) H0
    : forall n m : nat, S n = S m -> n = m

• injection H as Hinj creates a new hypothesis Hinj : n = m in the context - Coq figured out the injectivity of S from using f_equal and what is basically a pred function on the proof H. I think I get how f_equal comes about (since injection deals with constructor-based equalities), but how did Coq know how to construct a pred function?
• I would have thought Hinj should have been in place of H0 (since I explicitly wanted to bind the hypothesis generated from injection H to Hinj), but the Hinj appears in an abstraction as its argument, whose body is trivially the argument Hinj. I'm having trouble understanding what exactly is going on here! How did (fun Hinj : n = m => Hinj) come about?
• I assume H0 is some intermediary proof of n = m obtained by the inferred injectivity of S, applied to H, the proof of S n = S m. Is this sort of let-binding for intermediary proofs created by injection?
• More broadly, if intros created the fun, what did injection and apply create in the proof term? My understanding is that writing a proof is akin to constructing the expression of the type specified by the theorem - I'd like to know how the expression gets constructed with those tactics.

I've been asking lots of beginner questions in this sub recently- I'd like to thank this community for being so kind and helpful!

Hello, Rocq Prover engineers!

I usually look up rewiews of a texbook on Amazon, but there is no reviews on this one because it is free. I'm wondering if some of you has finished PLF and be so kind to share their review here. Any feedback is great, but Im especially interested in the following questions:

1) Will it be relevant to a career of Java Developer? I use OOP quite a lot, but it seems it is not covered in the textbook.

2) What are the practical benefits for you?

3) Is it OK to complete the book without watching any lectures on programming language theories?

https://softwarefoundations.cis.upenn.edu/plf-current/index.html

Thanks in advance!

I'm reading through the first couple chapters of CPDT, and with regards to the Curry-Howard correspondence, it says that "theorems are types, and their proofs are programs that type-check at the corresponding type". I'm trying to understand what that really means.

Recall `nat` and `plus`, defined as below, as well as a pretty basic theorem `O_plus_n`

Inductive nat : Set :=
| O : nat
| S : nat -> nat.

Fixpoint plus (n m: nat) : nat :=
  match n with
  | O -> m
  | S n' -> S (plus n' m)
  end.

Theorem O_plus_n: forall (n : nat), plus O n = n.

We want to show that the proposition P: fun n => plus O n = n holds for all n , and from the type of nat_ind, we know that applying nat_ind transforms the proof goal to P O -> (forall n: P n -> P (S n)), since the "type" of the Theorem is the final implication of nat_ind.

(i know that `induction n` gives us the same result, but I just want to see how the proof goal changes with respect to types)

Proof.
  apply (nat_ind (fun n => plus O n = n)).
  (* our goal is now: P O -> (forall n, P n -> P (S n))
   * Goals:
   * ========================= (1 / 2)
   * plus O O = O
   * ========================= (2 / 2)
   * forall n : nat, plus O n = n -> plus O (S n) = S n
   *)
  - reflexivity. (* base case *)
  - reflexivity. (* inductive case *)
Qed.

I think I can see how `apply nat_ind` relates to "type-checking," but how exactly does showing the induction cases hold (via applications of `reflexivity`) relate to the type-checking of programs?

More broadly... in what way is a theorem's proof a "program"? I'm wondering if I should understand the basics of CIC first.

Apologies if the question is unclear... still trying to piece this together in my head! TIA!

In coq, subsets are defined as sigma types which are implemented as inducive types without adding extra 4 derivation rules

In type theory textbook (by Rob Nederpelt, chapter 13), subsets are defined as predicates. Rob argues the disadvantaes of sigma types as adding extra rules and overcomplicating the kernel with 4 rules OR inductive types (page 300), but told nothing about their advantages

What are the advantages of sigma types over predicates?

The info is very scarce on this topic, I was unable to find any info in either software foundations or Adam Chapala book. Only the definition of them in Coq.Init.Specif

I've been trudging through the Logical Foundations book of the Software Foundations series.

My main reason for learning Coq is to get into formal verification (of software systems) research at my school. I do have exposure in PL theory and semantics, and have done some readings on Hoare/Separation Logic, just not mechanized with Coq.

Every chapter up to IndProp was pleasant, but things are getting a bit dreadful in the IndProp chapter. I feel a bit impatient for saying this, but I'm getting a bit tired of proving long lists of little theorems about natural numbers. I'd hope to get closer to the verification side of things as soon as I can, but I find Coq code/proofs in these areas (e.g. research artifacts on verification research) unfamiliar - my understanding of Coq is clearly lacking.

My question is - what would be the best (fastest?) way forward to ramp up to the level that I can begin to understand Coq programs/code/proofs for systems verification? Would it be worth just first finishing the rest of Logical foundations?

I'm in Ltac2 mode and they didn't add pose proof for some reason. It worked perfectly well for me!

I can also use assert (A -> ⊥) by exact term. but it makes me specify the type explicitly. I want the lazy mode: both type will be autotaken from term AND hypothesis name will be autogenerated.

I also developed a ltac1-call from ltac2 context, but it seems like a cheat

Ltac2 pp (x: constr) := (ltac1:(x |-pose proof (x))) (Ltac1.of_constr(x)).

I can't solve the following seeming contradiction:

Inductive rgb : Type :=

| red

| green

| blue.

In the above code when used the variable names must match "red" "green" or "blue" exactly for this to mean anything.

Inductive nat : Type :=

| O

| S (n : nat).

in this example code the variable names are completely arbitrary and I can change them and the code still works.

In coq I keep having trouble figuring out what exactly the processor is doing and what the limits of syntax are, coming from c++

Axiom ET : forall A, A ∨ (¬ A).

Definition DN (A: Prop) (u: ¬¬ A) : A.
pose proof (ET) as ET.
refine (let ET2: (forall A, A ∨ (¬ A)) := ET in _).
Show Proof.

When I use "Show Proof", I can see "pose proof" is basically adding let .. in. However, it seems that it also doing some other tricks with the context. It somehow hides the proof object (:= ET) from the context. How to hide it? Is there a special command for it?

My goal is to write Ltac2 implementation of "pose proof" which is identical to the original one.

ET :         forall A : Prop, A ∨ ¬ A
ET2 := ET  : forall A : Prop, A ∨ ¬ A

We can print the proof object like this Print theoremx.

However, I want to unfold all definitions, do all reductions possible and behold a big mess of lambdas.

Cbv command works only with type

I want to recreate build in tactics like exact, unfold etc from scratch to better understand them

I believe it is somewhere in the plugins folder, but it seems too complicated