search

meta-introspector / UniMath

This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
http://unimath.org/
Other
0 stars 0 forks source link

`assoc` #21

Open jmikedupont2 opened 10 months ago

jmikedupont2 commented 10 months ago

Goal: X : UU opp : binop X assoc : isassoc opp un0 : X unaxs : isunit opp un0 inv0 : X → X axs : isinv opp (unel_is (assoc,, un0,, unaxs)) inv0 x0 : X f := λ x : X, opp x0 x : X → X g := λ x : X, opp (inv0 x0) x : X → X ============================ (∏ x : X, g (f x) = x) DEBUG:Going to execute: PTRDEBUGTACcoq-core.plugins.ltac::intro@1 $1 DEBUG LTAC Evaluated term: (! assoc x (inv0 x0) x0) DEBUG LTAC Evaluated term: (pr1 axs x0) DEBUG LTAC Evaluated term: e DEBUG LTAC Evaluated term: e DEBUG LTAC Evaluated term: (pr2 unaxs x) DEBUG LTAC Evaluated term: (isweq_iso f g egf efg) DEBUG LTAC Evaluated term: is DEBUG LTAC Evaluated term: (λ x : X, opp x0 x) DEBUG LTAC Evaluated term: (λ x : X, opp (pr1 istr x0) x) DEBUG LTAC Evaluated term: is DEBUG LTAC Evaluated term: istr DEBUG LTAC Evaluated term: isun0 DEBUG LTAC Evaluated term: (∏ x : X, g (f x) = x) TcDebug (0) > NONE??? LtacNotationCall (no location),/mnt/data1/2024/01/05/UniMath/UniMath/Algebra/BinaryOperations.v:462

It seems like you have provided a Coq proof goal. Let's break it down:

Goal:

X : UU
opp : binop X
assoc : isassoc opp
un0 : X
unaxs : isunit opp un0
inv0 : X → X
axs : isinv opp (unel_is (assoc,, un0,, unaxs)) inv0
x0 : X
f := λ x : X, opp x0 x : X → X
g := λ x : X, opp (inv0 x0) x : X → X
============================
(∏ x : X, g (f x) = x)

This Coq goal states that for a given type X, a binary operation opp on X, proofs of associativity assoc, existence of a unit element un0, proofs of it being a unit unaxs, an inverse function inv0, and proofs of opp being invertible axs, an element x0 of type X, and two functions f and g defined as λ x : X, opp x0 x and λ x : X, opp (inv0 x0) x, respectively, we need to prove that for every x : X, g (f x) = x.

The debug output you provided seems to be related to the execution of tactics in Coq, but without more context, it's difficult to determine the exact meaning of the debug information.

If you have any specific questions or need assistance with the proof, please let me know, and I'll be happy to help!