Prove a Theorem in HashMath

You are helping the user prove a theorem in the HashMath proof assistant.

Key Facts About HashMath

HashMath is a Calculus of Inductive Constructions (CIC) kernel. There are NO tactics — all proofs are explicit proof terms (lambda calculus + recursors).

Proof Techniques

Recursor elimination: The primary proof method. Each inductive type T has T.rec. Example: Nat.rec.{1} (fun (_ : Nat) => Nat) base_case step_case n
Eq.rec: For equality proofs. Eq.rec.{1} A a (fun (x : A) (_ : Eq A a x) => P x) base_proof b eq_proof
Large elimination: Some Prop types allow computing Type-valued results (Eq, And, etc.)
Definitional reduction: #eval normalizes; use it to check computational behavior

Universe Gotchas

Prove a Theorem in HashMath

You are helping the user prove a theorem in the HashMath proof assistant.

Key Facts About HashMath

HashMath is a Calculus of Inductive Constructions (CIC) kernel. There are NO tactics — all proofs are explicit proof terms (lambda calculus + recursors).

Proof Techniques

Recursor elimination: The primary proof method. Each inductive type T has T.rec. Example: Nat.rec.{1} (fun (_ : Nat) => Nat) base_case step_case n
Eq.rec: For equality proofs. Eq.rec.{1} A a (fun (x : A) (_ : Eq A a x) => P x) base_proof b eq_proof
Large elimination: Some Prop types allow computing Type-valued results (Eq, And, etc.)
Definitional reduction: #eval normalizes; use it to check computational behavior

Hm Prove

Prove a Theorem in HashMath

Key Facts About HashMath

Proof Techniques

Universe Gotchas

Hm Prove

Prove a Theorem in HashMath

Key Facts About HashMath

Proof Techniques

Universe Gotchas

Standard Library

Workflow

Important: Iterate

Argument: $ARGUMENTS

Update Skills

Eval Harness

Ecc Tools Cost Audit

Code Tour

Rules Distill

Design System