Stream: Coq users

Topic: Use of In


view this post on Zulip pianke (Apr 15 2023 at 19:25):

I have natural number list l1: [a1,a2,a3 ..an] which undergoes a test condition in the form of function f( m n o:nat l:list nat). As a result some elements get drop and get valid list l2:[b1,b2..bn]. Any element of l1 which follows the condition must present in l2.
Any x of l1 (In x l1) during simplification get this form x=a1\/In x l1.. i have problem in identifying first element.
because after test result (in l2) it has different name or may be drop. How to identify it? Use any other function instead of In x l1?

view this post on Zulip Bhakti Shah (Apr 16 2023 at 05:23):

Sorry, what exactly are you trying to prove? I'm having trouble understanding your use case - you have a list that is filtered on some condition and you get a new list with only the elements that satisfy the condition - are you trying to prove that any element that satisfies the condition must be in the new list? or do you mean something else

view this post on Zulip Laurent Théry (Apr 16 2023 at 08:54):

Again @pianke, try to provide valid Coq code with your question. Is your problem that you are trying to prove this?

Require Import List.
Import ListNotations.

Parameter f : list nat -> list nat.
Parameter check : nat -> bool.

Goal forall x l, In x l -> check x = true -> In x (f l).

Last updated: Mar 28 2024 at 22:01 UTC