The Coq mailing list

[Jan Bessai <jan.bessai AT tu-dortmund.de>]

Thorsten,

perhaps the technique presented by Larchey-Wendling and Monin at Types
2018 "Simulating Induction-Recursion for Partial Algorithms" [1] can
help you. Their trick is to use an inductively defined relation instead
of a function and later show that the relation is in fact a terminating
function. In your case you might be able to prove facts about the
relation to proceed.
Or you could have a tactic (which doesn't require any termination proof)
to infer an instance of their termination predicate D, which makes the
recursive calls proceed for the specific case you are interested in.
Also, here [2] is a larger example, where I used it to implement an
algorithm for intersection type subtyping. I can send you a paper
(accepted and to appear soon) describing the code if you are interested.

-- Jan

[1]:
https://types2018.projj.eu/wp-content/uploads/2018/06/BookOfAbstractsTYPES2018.pdf
[2]: https://github.com/JanBessai/SubtypeMachine/blob/github/Types.v


On 01.11.18 12:21, Thorsten Altenkirch wrote:
> Is there a way to run possibly non-terminating programs in the coq type 
> checker. In Agda you can just switch off the termination checker.
> 
> I think this is useful if you want to use something whose termination you 
> haven't yet proven but want to exploit reduction.
> 
> Hence it is not enough to add the assumption that it terminates as an axiom 
> because this won't reduce.
> 
> Thorsten
> 
> 
> 
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment. 
> 
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored 
> where permitted by law.
> 
> 
> 
> 

-- 
Jan Bessai (M.Sc.)
Wissenschaftlicher Mitarbeiter

Technische Universität Dortmund
Fakultät für Informatik - Lehrstuhl 14 Software Engineering
Otto-Hahn Straße 14
D-44227 Dortmund

Tel.: +49 231-755 77 64
Fax: +49 231-755 79 36
jan.bessai AT tu-dortmund.de
www.tu-dortmund.de


Wichtiger Hinweis: Die Information in dieser E-Mail ist vertraulich. Sie
ist ausschließlich für den Adressaten bestimmt. Sollten Sie nicht der
für diese E-Mail bestimmte Adressat sein, unterrichten Sie bitte den
Absender und vernichten Sie diese Mail. Vielen Dank.
Unbeschadet der Korrespondenz per E-Mail, sind unsere Erklärungen
ausschließlich final rechtsverbindlich, wenn sie in herkömmlicher
Schriftform (mit eigenhändiger Unterschrift) oder durch Übermittlung
eines solchen Schriftstücks per Telefax erfolgen.

Important note: The information included in this e-mail is confidential.
It is solely intended for the recipient. If you are not the intended
recipient of this e-mail please contact the sender and delete this
message. Thank you.
Without prejudice of e-mail correspondence, our statements are only
legally binding when they are made in the conventional written form
(with personal signature) or when such documents are sent by fax.